Isabelle에서 3x3 행렬 정의하기

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에는 꽤 발전된 매트릭스 라이브러리가 있습니다.

다른 행렬 치수가 수학과 같이 부분 공간에 대한 술어와 함께 균일 한 스키마로 덮여 있기 때문에 특히 좋습니다.