Isabelleで3行3列の行列を定義する

Question

私は正式な証明のためにIsabelleを使用する初心者です。ベクトルと3×3行列の乗算が必要です。今

、私は私の質問は3行列によって3を定義する方法である

'consts x_vec :: "('a::real_vector) set ⇒ ('a ⇒ real×real×real) ⇒ bool"' 

このコマンドを使用して、3要素のベクトルを定義することができています。私が作業しなければならない行列は慣性行列です。

Answer 1

Archive of Formal Proofsには非常に高度なマトリックスライブラリがあります。

さまざまな行列の次元が、数学のように部分空間の述語を持つ均一型スキームでカバーされているので、特にうれしいです。