FinMatrix.Matrix.MatrixQc
Include (NormedOrderedFieldMatrixTheory NormedOrderedFieldElementTypeQc).
Open Scope Q_scope.
Open Scope Qc_scope.
Open Scope vec_scope.
Open Scope mat_scope.
Section test.
Open Scope vec_scope.
Let u := @l2v 3 (listQ2Qc [1; 2; 3]%Q).
Let v := @l2v 3 (listQ2Qc [2; 1; 0]%Q).
Open Scope mat_scope.
Let M := @l2m 3 3 (dlistQ2Qc [[1;-3;-2];[-2;1;-4];[-1;4;-1]]%Q).
Example 1: inverse matrix of a `3x3` matrix over Qc type
Section ex1.
Let l1 := dlistQ2Qc [[1;3;1];[2;1;1];[2;2;1]]%Q.
Let l2 := dlistQ2Qc [[-1;-1;2];[0;-1;1];[2;4;-5]]%Q.
Let M1 : smat 3 := l2m l1.
Let M2 : smat 3 := l2m l2.
Goal minvAM M1 = M2.
Proof. meq. Qed.
End ex1.
Section ex2.
Let A : smat 2 := l2m (dlistQ2Qc [[1;2];[3;4]]%Q).
Let b : vec 2 := l2v (listQ2Qc [5;6]%Q).
End ex2.
Section ex3.
Let M2 : smat 5 :=
l2m (dlistQ2Qc
[[1;2;3;4;5];
[2;4;3;5;1];
[3;1;5;2;4];
[4;5;2;3;1];
[5;4;1;2;3]]%Q).
Let b2 : vec 5 := l2v (listQ2Qc [1;2;3;5;4]%Q).
End ex3.
End test.
Let l1 := dlistQ2Qc [[1;3;1];[2;1;1];[2;2;1]]%Q.
Let l2 := dlistQ2Qc [[-1;-1;2];[0;-1;1];[2;4;-5]]%Q.
Let M1 : smat 3 := l2m l1.
Let M2 : smat 3 := l2m l2.
Goal minvAM M1 = M2.
Proof. meq. Qed.
End ex1.
Section ex2.
Let A : smat 2 := l2m (dlistQ2Qc [[1;2];[3;4]]%Q).
Let b : vec 2 := l2v (listQ2Qc [5;6]%Q).
End ex2.
Section ex3.
Let M2 : smat 5 :=
l2m (dlistQ2Qc
[[1;2;3;4;5];
[2;4;3;5;1];
[3;1;5;2;4];
[4;5;2;3;1];
[5;4;1;2;3]]%Q).
Let b2 : vec 5 := l2v (listQ2Qc [1;2;3;5;4]%Q).
End ex3.
End test.