(real,'n) vecのベクトルをFinite_Cartesian_Product理論に転置するための定義または補題が見つかりませんでした。私は転置行列を転置行列とベクトルで置き換えようとしています。例えば、e = A xの転置と（e^T）の転置は、転置の結果としてAとx（e^T = A^T x^T）になります。 Isabelle/HOLでこれを行うことはできますか？私はあなたが定数を見てお勧め：すべてのIsabelle/HOLでのベクトル転置
まず、私の線形代数は完全に今の私を失敗している場合を除き、(AB)^T = B^T A^T、ないA^T B^Tので、あなたの第2式はe^T = x^T A^T
はあなたの実際の質問に答えるためにする必要がありますrowvector,columnvectorおよびtransposeから~~/src/HOL/Analysis/Cartesian_Euclidean_Spaceまでである。最初の2つは、長さがnのベクトルを1 × n（resp。n × 1）の行列に変換することを可能にし、後者は行列を転置することができます。
e = A xはcolumnvector e = A ** columnvector x、e^T = x^T A^Tはrowvector e = rowvector x ** transpose Aのようです。