在Isabelle中定義3乘3矩陣

Question

我是使用Isabelle進行正式證明的初學者。我必須在矢量和3×3矩陣之間進行乘法運算。

現在，我可以使用此命令

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

我的問題是如何通過3矩陣定義3定義3元向量。我需要處理的矩陣是慣性矩陣。

Answer 1

Archive of Formal Proofs中有一個相當先進的矩陣庫。

這是特別好的，因爲不同的矩陣尺寸被一個統一的類型方案所覆蓋，其中子空間的謂詞和數學一樣。