Isabelle/HOL中的向量轉置

Question

我找不到在Finite_Cartesian_Product理論中轉置(real,'n) vec類型向量的定義或引理。例如，如果矢量e = A x然後是e（e^T）的轉置導致轉置A和x（e^T = A^T x^T），我試圖用轉置矩陣和矢量來代替轉置矢量。我可以在Isabelle/HOL中做到這一點嗎？

Answer 1

首先，除非我的線性代數是完全沒有我現在，(AB)^T = B^T A^T，不A^T B^T，那麼你的第二個公式應該是e^T = x^T A^T

爲了回答您的實際問題：我建議你看看常數rowvector，columnvector和transpose，從~~/src/HOL/Analysis/Cartesian_Euclidean_Space。前兩個允許您將長度爲n的矢量轉換爲1 × n（或n × 1）矩陣，後者允許您轉置矩陣。

我想你的e = A x看起來像columnvector e = A ** columnvector x和你的e^T = x^T A^T將rowvector e = rowvector x ** transpose A。