From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.algebra.matrix.html | 1546 +++++++++++++++--------------
1 file changed, 781 insertions(+), 765 deletions(-)
(limited to 'docs/htmldoc/mathcomp.algebra.matrix.html')
diff --git a/docs/htmldoc/mathcomp.algebra.matrix.html b/docs/htmldoc/mathcomp.algebra.matrix.html
index 05ce5f3..0733b20 100644
--- a/docs/htmldoc/mathcomp.algebra.matrix.html
+++ b/docs/htmldoc/mathcomp.algebra.matrix.html
@@ -21,7 +21,6 @@
@@ -238,7 +237,7 @@ Type Definition*********************************
Variable R : Type.
-Variables m n : nat.
+Variables m n : nat.
@@ -251,104 +250,109 @@ Type Definition*********************************
-
Inductive matrix :
predArgType :=
Matrix of {ffun 'I_m × 'I_n → R}.
+
Inductive matrix :
predArgType :=
Matrix of {ffun 'I_m × 'I_n → R}.
Definition mx_val A :=
let:
Matrix g :=
A in g.
-
Canonical matrix_subType :=
Eval hnf in [newType for mx_val].
+
Canonical matrix_subType :=
Eval hnf in [newType for mx_val].
-
Fact matrix_key :
unit.
-
Definition matrix_of_fun_def F :=
Matrix [ffun ij ⇒ F ij.1 ij.2].
-
Definition matrix_of_fun k :=
locked_with k matrix_of_fun_def.
-
Canonical matrix_unlockable k :=
[unlockable fun matrix_of_fun k].
+
Fact matrix_key :
unit.
+
Definition matrix_of_fun_def F :=
Matrix [ffun ij ⇒ F ij.1 ij.2].
+
Definition matrix_of_fun k :=
locked_with k matrix_of_fun_def.
+
Canonical matrix_unlockable k :=
[unlockable fun matrix_of_fun k].
-
Definition fun_of_matrix A (
i :
'I_m) (
j :
'I_n) :=
mx_val A (i, j).
+
Definition fun_of_matrix A (
i :
'I_m) (
j :
'I_n) :=
mx_val A (i, j).
Coercion fun_of_matrix : matrix >-> Funclass.
-
Lemma mxE k F :
matrix_of_fun k F =2 F.
+
Lemma mxE k F :
matrix_of_fun k F =2 F.
-
Lemma matrixP (
A B :
matrix) :
A =2 B ↔ A = B.
+
Lemma matrixP (
A B :
matrix) :
A =2 B ↔ A = B.
+
+
Lemma eq_mx k F1 F2 :
(F1 =2 F2) → matrix_of_fun k F1 = matrix_of_fun k F2.
+
End MatrixDef.
-
Notation "''M[' R ]_ ( m , n )" := (
matrix R m n) (
only parsing):
type_scope.
-
Notation "''rV[' R ]_ n" :=
'M[R]_(1
, n) (
only parsing) :
type_scope.
-
Notation "''cV[' R ]_ n" :=
'M[R]_(n, 1
) (
only parsing) :
type_scope.
-
Notation "''M[' R ]_ n" :=
'M[R]_(n, n) (
only parsing) :
type_scope.
-
Notation "''M[' R ]_ ( n )" :=
'M[R]_n (
only parsing) :
type_scope.
-
Notation "''M_' ( m , n )" :=
'M[_]_(m, n) :
type_scope.
-
Notation "''rV_' n" :=
'M_(1
, n) :
type_scope.
-
Notation "''cV_' n" :=
'M_(n, 1
) :
type_scope.
-
Notation "''M_' n" :=
'M_(n, n) :
type_scope.
-
Notation "''M_' ( n )" :=
'M_n (
only parsing) :
type_scope.
-
Notation "\matrix[ k ]_ ( i , j ) E" := (
matrix_of_fun k (
fun i j ⇒
E))
+
Notation "''M[' R ]_ ( m , n )" := (
matrix R m n) (
only parsing):
type_scope.
+
Notation "''rV[' R ]_ n" :=
'M[R]_(1
, n) (
only parsing) :
type_scope.
+
Notation "''cV[' R ]_ n" :=
'M[R]_(n, 1
) (
only parsing) :
type_scope.
+
Notation "''M[' R ]_ n" :=
'M[R]_(n, n) (
only parsing) :
type_scope.
+
Notation "''M[' R ]_ ( n )" :=
'M[R]_n (
only parsing) :
type_scope.
+
Notation "''M_' ( m , n )" :=
'M[_]_(m, n) :
type_scope.
+
Notation "''rV_' n" :=
'M_(1
, n) :
type_scope.
+
Notation "''cV_' n" :=
'M_(n, 1
) :
type_scope.
+
Notation "''M_' n" :=
'M_(n, n) :
type_scope.
+
Notation "''M_' ( n )" :=
'M_n (
only parsing) :
type_scope.
+
+
+
Notation "\matrix[ k ]_ ( i , j ) E" := (
matrix_of_fun k (
fun i j ⇒
E))
(
at level 36,
E at level 36,
i,
j at level 50):
ring_scope.
-
Notation "\matrix_ ( i < m , j < n ) E" :=
+
Notation "\matrix_ ( i < m , j < n ) E" :=
(@
matrix_of_fun _ m n matrix_key (
fun i j ⇒
E)) (
only parsing) :
ring_scope.
-
Notation "\matrix_ ( i , j < n ) E" :=
- (
\matrix_(i < n, j < n) E) (
only parsing) :
ring_scope.
+
Notation "\matrix_ ( i , j < n ) E" :=
+ (
\matrix_(i < n, j < n) E) (
only parsing) :
ring_scope.
-
Notation "\matrix_ ( i , j ) E" := (
\matrix_(i < _, j < _) E) :
ring_scope.
+
Notation "\matrix_ ( i , j ) E" := (
\matrix_(i < _, j < _) E) :
ring_scope.
-
Notation "\matrix_ ( i < m ) E" :=
- (
\matrix_(i < m, j < _) @
fun_of_matrix _ 1
_ E 0
j)
+
Notation "\matrix_ ( i < m ) E" :=
+ (
\matrix_(i < m, j < _) @
fun_of_matrix _ 1
_ E 0
j)
(
only parsing) :
ring_scope.
-
Notation "\matrix_ i E" := (
\matrix_(i < _) E) :
ring_scope.
+
Notation "\matrix_ i E" := (
\matrix_(i < _) E) :
ring_scope.
-
Notation "\col_ ( i < n ) E" := (@
matrix_of_fun _ n 1
matrix_key (
fun i _ ⇒
E))
+
Notation "\col_ ( i < n ) E" := (@
matrix_of_fun _ n 1
matrix_key (
fun i _ ⇒
E))
(
only parsing) :
ring_scope.
-
Notation "\col_ i E" := (
\col_(i < _) E) :
ring_scope.
+
Notation "\col_ i E" := (
\col_(i < _) E) :
ring_scope.
-
Notation "\row_ ( j < n ) E" := (@
matrix_of_fun _ 1
n matrix_key (
fun _ j ⇒
E))
+
Notation "\row_ ( j < n ) E" := (@
matrix_of_fun _ 1
n matrix_key (
fun _ j ⇒
E))
(
only parsing) :
ring_scope.
-
Notation "\row_ j E" := (
\row_(j < _) E) :
ring_scope.
+
Notation "\row_ j E" := (
\row_(j < _) E) :
ring_scope.
Definition matrix_eqMixin (
R :
eqType)
m n :=
-
Eval hnf in [eqMixin of 'M[R]_(m, n) by <:].
+
Eval hnf in [eqMixin of 'M[R]_(m, n) by <:].
Canonical matrix_eqType (
R :
eqType)
m n:=
-
Eval hnf in EqType 'M[R]_(m, n) (
matrix_eqMixin R m n).
+
Eval hnf in EqType 'M[R]_(m, n) (
matrix_eqMixin R m n).
Definition matrix_choiceMixin (
R :
choiceType)
m n :=
-
[choiceMixin of 'M[R]_(m, n) by <:].
+
[choiceMixin of 'M[R]_(m, n) by <:].
Canonical matrix_choiceType (
R :
choiceType)
m n :=
-
Eval hnf in ChoiceType 'M[R]_(m, n) (
matrix_choiceMixin R m n).
+
Eval hnf in ChoiceType 'M[R]_(m, n) (
matrix_choiceMixin R m n).
Definition matrix_countMixin (
R :
countType)
m n :=
-
[countMixin of 'M[R]_(m, n) by <:].
+
[countMixin of 'M[R]_(m, n) by <:].
Canonical matrix_countType (
R :
countType)
m n :=
-
Eval hnf in CountType 'M[R]_(m, n) (
matrix_countMixin R m n).
+
Eval hnf in CountType 'M[R]_(m, n) (
matrix_countMixin R m n).
Canonical matrix_subCountType (
R :
countType)
m n :=
-
Eval hnf in [subCountType of 'M[R]_(m, n)].
+
Eval hnf in [subCountType of 'M[R]_(m, n)].
Definition matrix_finMixin (
R :
finType)
m n :=
-
[finMixin of 'M[R]_(m, n) by <:].
+
[finMixin of 'M[R]_(m, n) by <:].
Canonical matrix_finType (
R :
finType)
m n :=
-
Eval hnf in FinType 'M[R]_(m, n) (
matrix_finMixin R m n).
+
Eval hnf in FinType 'M[R]_(m, n) (
matrix_finMixin R m n).
Canonical matrix_subFinType (
R :
finType)
m n :=
-
Eval hnf in [subFinType of 'M[R]_(m, n)].
+
Eval hnf in [subFinType of 'M[R]_(m, n)].
-
Lemma card_matrix (
F :
finType)
m n : (
#|{: 'M[F]_(m, n)}| = #|F| ^ (m × n))%
N.
+
Lemma card_matrix (
F :
finType)
m n : (
#|{: 'M[F]_(m, n)}| = #|F| ^ (m × n))%
N.
@@ -371,8 +375,8 @@ Type Definition*********************************
Constant matrix
-
Definition castmx m' n' (
eq_mn :
(m = m') × (n = n'))
A :
'M_(m', n') :=
-
let:
erefl in _ = m' :=
eq_mn.1 return 'M_(m', n') in
-
let:
erefl in _ = n' :=
eq_mn.2 return 'M_(m, n') in A.
+
Definition castmx m' n' (
eq_mn :
(m = m') × (n = n'))
A :
'M_(m', n') :=
+
let:
erefl in _ = m' :=
eq_mn.1 return 'M_(m', n') in
+
let:
erefl in _ = n' :=
eq_mn.2 return 'M_(m, n') in A.
Definition conform_mx m' n' B A :=
-
match m =P m',
n =P n' with
- |
ReflectT eq_m,
ReflectT eq_n ⇒
castmx (eq_m, eq_n) A
+
match m =P m',
n =P n' with
+ |
ReflectT eq_m,
ReflectT eq_n ⇒
castmx (eq_m, eq_n) A
|
_,
_ ⇒
B
end.
@@ -412,8 +416,8 @@ Type Definition*********************************
Transpose a matrix
-
Definition row' i0 A :=
\matrix_(i, j) A (
lift i0 i)
j.
-
Definition col' j0 A :=
\matrix_(i, j) A i (
lift j0 j).
+
Definition row' i0 A :=
\matrix_(i, j) A (
lift i0 i)
j.
+
Definition col' j0 A :=
\matrix_(i, j) A i (
lift j0 j).
-
Lemma castmx_const m' n' (
eq_mn :
(m = m') × (n = n'))
a :
-
castmx eq_mn (
const_mx a)
= const_mx a.
+
Lemma castmx_const m' n' (
eq_mn :
(m = m') × (n = n'))
a :
+
castmx eq_mn (
const_mx a)
= const_mx a.
-
Lemma trmx_const a :
trmx (
const_mx a)
= const_mx a.
+
Lemma trmx_const a :
trmx (
const_mx a)
= const_mx a.
-
Lemma row_perm_const s a :
row_perm s (
const_mx a)
= const_mx a.
+
Lemma row_perm_const s a :
row_perm s (
const_mx a)
= const_mx a.
-
Lemma col_perm_const s a :
col_perm s (
const_mx a)
= const_mx a.
+
Lemma col_perm_const s a :
col_perm s (
const_mx a)
= const_mx a.
-
Lemma xrow_const i1 i2 a :
xrow i1 i2 (
const_mx a)
= const_mx a.
+
Lemma xrow_const i1 i2 a :
xrow i1 i2 (
const_mx a)
= const_mx a.
-
Lemma xcol_const j1 j2 a :
xcol j1 j2 (
const_mx a)
= const_mx a.
+
Lemma xcol_const j1 j2 a :
xcol j1 j2 (
const_mx a)
= const_mx a.
-
Lemma rowP (
u v :
'rV[R]_n) :
u 0
=1 v 0
↔ u = v.
+
Lemma rowP (
u v :
'rV[R]_n) :
u 0
=1 v 0
↔ u = v.
-
Lemma rowK u_ i0 :
row i0 (
\matrix_i u_ i)
= u_ i0.
+
Lemma rowK u_ i0 :
row i0 (
\matrix_i u_ i)
= u_ i0.
-
Lemma row_matrixP A B :
(∀ i,
row i A = row i B) ↔ A = B.
+
Lemma row_matrixP A B :
(∀ i,
row i A = row i B) ↔ A = B.
-
Lemma colP (
u v :
'cV[R]_m) :
u^~ 0
=1 v^~ 0
↔ u = v.
+
Lemma colP (
u v :
'cV[R]_m) :
u^~ 0
=1 v^~ 0
↔ u = v.
-
Lemma row_const i0 a :
row i0 (
const_mx a)
= const_mx a.
+
Lemma row_const i0 a :
row i0 (
const_mx a)
= const_mx a.
-
Lemma col_const j0 a :
col j0 (
const_mx a)
= const_mx a.
+
Lemma col_const j0 a :
col j0 (
const_mx a)
= const_mx a.
-
Lemma row'_const i0 a :
row' i0 (
const_mx a)
= const_mx a.
+
Lemma row'_const i0 a :
row' i0 (
const_mx a)
= const_mx a.
-
Lemma col'_const j0 a :
col' j0 (
const_mx a)
= const_mx a.
+
Lemma col'_const j0 a :
col' j0 (
const_mx a)
= const_mx a.
-
Lemma col_perm1 A :
col_perm 1
A = A.
+
Lemma col_perm1 A :
col_perm 1
A = A.
-
Lemma row_perm1 A :
row_perm 1
A = A.
+
Lemma row_perm1 A :
row_perm 1
A = A.
-
Lemma col_permM s t A :
col_perm (
s × t)
A = col_perm s (
col_perm t A).
+
Lemma col_permM s t A :
col_perm (
s × t)
A = col_perm s (
col_perm t A).
-
Lemma row_permM s t A :
row_perm (
s × t)
A = row_perm s (
row_perm t A).
+
Lemma row_permM s t A :
row_perm (
s × t)
A = row_perm s (
row_perm t A).
Lemma col_row_permC s t A :
-
col_perm s (
row_perm t A)
= row_perm t (
col_perm s A).
+
col_perm s (
row_perm t A)
= row_perm t (
col_perm s A).
End FixedDim.
@@ -522,21 +526,21 @@ Type Definition*********************************
-
Lemma castmx_id m n erefl_mn (
A :
'M_(m, n)) :
castmx erefl_mn A = A.
+
Lemma castmx_id m n erefl_mn (
A :
'M_(m, n)) :
castmx erefl_mn A = A.
-
Lemma castmx_comp m1 n1 m2 n2 m3 n3 (
eq_m1 :
m1 = m2) (
eq_n1 :
n1 = n2)
- (
eq_m2 :
m2 = m3) (
eq_n2 :
n2 = n3)
A :
-
castmx (eq_m2, eq_n2) (
castmx (eq_m1, eq_n1) A)
-
= castmx (etrans eq_m1 eq_m2, etrans eq_n1 eq_n2) A.
+
Lemma castmx_comp m1 n1 m2 n2 m3 n3 (
eq_m1 :
m1 = m2) (
eq_n1 :
n1 = n2)
+ (
eq_m2 :
m2 = m3) (
eq_n2 :
n2 = n3)
A :
+
castmx (eq_m2, eq_n2) (
castmx (eq_m1, eq_n1) A)
+
= castmx (etrans eq_m1 eq_m2, etrans eq_n1 eq_n2) A.
-
Lemma castmxK m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2) :
-
cancel (
castmx (eq_m, eq_n)) (
castmx (esym eq_m, esym eq_n)).
+
Lemma castmxK m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2) :
+
cancel (
castmx (eq_m, eq_n)) (
castmx (esym eq_m, esym eq_n)).
-
Lemma castmxKV m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2) :
-
cancel (
castmx (esym eq_m, esym eq_n)) (
castmx (eq_m, eq_n)).
+
Lemma castmxKV m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2) :
+
cancel (
castmx (esym eq_m, esym eq_n)) (
castmx (eq_m, eq_n)).
-
Lemma castmx_sym m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2)
A1 A2 :
-
A1 = castmx (eq_m, eq_n) A2 → A2 = castmx (esym eq_m, esym eq_n) A1.
+
Lemma castmx_sym m1 n1 m2 n2 (
eq_m :
m1 = m2) (
eq_n :
n1 = n2)
A1 A2 :
+
A1 = castmx (eq_m, eq_n) A2 → A2 = castmx (esym eq_m, esym eq_n) A1.
-
Lemma castmxE m1 n1 m2 n2 (
eq_mn :
(m1 = m2) × (n1 = n2))
A i j :
-
castmx eq_mn A i j =
-
A (
cast_ord (
esym eq_mn.1)
i) (
cast_ord (
esym eq_mn.2)
j).
+
Lemma castmxE m1 n1 m2 n2 (
eq_mn :
(m1 = m2) × (n1 = n2))
A i j :
+
castmx eq_mn A i j =
+
A (
cast_ord (
esym eq_mn.1)
i) (
cast_ord (
esym eq_mn.2)
j).
-
Lemma conform_mx_id m n (
B A :
'M_(m, n)) :
conform_mx B A = A.
+
Lemma conform_mx_id m n (
B A :
'M_(m, n)) :
conform_mx B A = A.
-
Lemma nonconform_mx m m' n n' (
B :
'M_(m', n')) (
A :
'M_(m, n)) :
-
(m != m') || (n != n') → conform_mx B A = B.
+
Lemma nonconform_mx m m' n n' (
B :
'M_(m', n')) (
A :
'M_(m, n)) :
+
(m != m') || (n != n') → conform_mx B A = B.
Lemma conform_castmx m1 n1 m2 n2 m3 n3
- (
e_mn :
(m2 = m3) × (n2 = n3)) (
B :
'M_(m1, n1))
A :
-
conform_mx B (
castmx e_mn A)
= conform_mx B A.
+ (
e_mn :
(m2 = m3) × (n2 = n3)) (
B :
'M_(m1, n1))
A :
+
conform_mx B (
castmx e_mn A)
= conform_mx B A.
-
Lemma trmxK m n :
cancel (@
trmx m n) (@
trmx n m).
+
Lemma trmxK m n :
cancel (@
trmx m n) (@
trmx n m).
-
Lemma trmx_inj m n :
injective (@
trmx m n).
+
Lemma trmx_inj m n :
injective (@
trmx m n).
-
Lemma trmx_cast m1 n1 m2 n2 (
eq_mn :
(m1 = m2) × (n1 = n2))
A :
-
(castmx eq_mn A)^T = castmx (eq_mn.2, eq_mn.1) A^T.
+
Lemma trmx_cast m1 n1 m2 n2 (
eq_mn :
(m1 = m2) × (n1 = n2))
A :
+
(castmx eq_mn A)^T = castmx (eq_mn.2, eq_mn.1) A^T.
-
Lemma tr_row_perm m n s (
A :
'M_(m, n)) :
(row_perm s A)^T = col_perm s A^T.
+
Lemma tr_row_perm m n s (
A :
'M_(m, n)) :
(row_perm s A)^T = col_perm s A^T.
-
Lemma tr_col_perm m n s (
A :
'M_(m, n)) :
(col_perm s A)^T = row_perm s A^T.
+
Lemma tr_col_perm m n s (
A :
'M_(m, n)) :
(col_perm s A)^T = row_perm s A^T.
-
Lemma tr_xrow m n i1 i2 (
A :
'M_(m, n)) :
(xrow i1 i2 A)^T = xcol i1 i2 A^T.
+
Lemma tr_xrow m n i1 i2 (
A :
'M_(m, n)) :
(xrow i1 i2 A)^T = xcol i1 i2 A^T.
-
Lemma tr_xcol m n j1 j2 (
A :
'M_(m, n)) :
(xcol j1 j2 A)^T = xrow j1 j2 A^T.
+
Lemma tr_xcol m n j1 j2 (
A :
'M_(m, n)) :
(xcol j1 j2 A)^T = xrow j1 j2 A^T.
-
Lemma row_id n i (
V :
'rV_n) :
row i V = V.
+
Lemma row_id n i (
V :
'rV_n) :
row i V = V.
-
Lemma col_id n j (
V :
'cV_n) :
col j V = V.
+
Lemma col_id n j (
V :
'cV_n) :
col j V = V.
-
Lemma row_eq m1 m2 n i1 i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
row i1 A1 = row i2 A2 → A1 i1 =1 A2 i2.
+
Lemma row_eq m1 m2 n i1 i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
row i1 A1 = row i2 A2 → A1 i1 =1 A2 i2.
-
Lemma col_eq m n1 n2 j1 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
col j1 A1 = col j2 A2 → A1^~ j1 =1 A2^~ j2.
+
Lemma col_eq m n1 n2 j1 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
col j1 A1 = col j2 A2 → A1^~ j1 =1 A2^~ j2.
-
Lemma row'_eq m n i0 (
A B :
'M_(m, n)) :
-
row' i0 A = row' i0 B → {in predC1 i0, A =2 B}.
+
Lemma row'_eq m n i0 (
A B :
'M_(m, n)) :
+
row' i0 A = row' i0 B → {in predC1 i0, A =2 B}.
-
Lemma col'_eq m n j0 (
A B :
'M_(m, n)) :
-
col' j0 A = col' j0 B → ∀ i,
{in predC1 j0, A i =1 B i}.
+
Lemma col'_eq m n j0 (
A B :
'M_(m, n)) :
+
col' j0 A = col' j0 B → ∀ i,
{in predC1 j0, A i =1 B i}.
-
Lemma tr_row m n i0 (
A :
'M_(m, n)) :
(row i0 A)^T = col i0 A^T.
+
Lemma tr_row m n i0 (
A :
'M_(m, n)) :
(row i0 A)^T = col i0 A^T.
-
Lemma tr_row' m n i0 (
A :
'M_(m, n)) :
(row' i0 A)^T = col' i0 A^T.
+
Lemma tr_row' m n i0 (
A :
'M_(m, n)) :
(row' i0 A)^T = col' i0 A^T.
-
Lemma tr_col m n j0 (
A :
'M_(m, n)) :
(col j0 A)^T = row j0 A^T.
+
Lemma tr_col m n j0 (
A :
'M_(m, n)) :
(col j0 A)^T = row j0 A^T.
-
Lemma tr_col' m n j0 (
A :
'M_(m, n)) :
(col' j0 A)^T = row' j0 A^T.
+
Lemma tr_col' m n j0 (
A :
'M_(m, n)) :
(col' j0 A)^T = row' j0 A^T.
Ltac split_mxE :=
apply/
matrixP⇒
i j;
do ![
rewrite mxE |
case:
split ⇒ ?].
@@ -628,7 +632,7 @@ Type Definition*********************************
Section CutPaste.
-
Variables m m1 m2 n n1 n2 :
nat.
+
Variables m m1 m2 n n1 n2 :
nat.
-
Fact row_mx_key :
unit.
-
Definition row_mx (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
'M[R]_(m, n1 + n2) :=
-
\matrix[row_mx_key]_(i, j)
-
match split j with inl j1 ⇒
A1 i j1 |
inr j2 ⇒
A2 i j2 end.
+
Fact row_mx_key :
unit.
+
Definition row_mx (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
'M[R]_(m, n1 + n2) :=
+
\matrix[row_mx_key]_(i, j)
+
match split j with inl j1 ⇒
A1 i j1 |
inr j2 ⇒
A2 i j2 end.
-
Fact col_mx_key :
unit.
-
Definition col_mx (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
'M[R]_(m1 + m2, n) :=
-
\matrix[col_mx_key]_(i, j)
-
match split i with inl i1 ⇒
A1 i1 j |
inr i2 ⇒
A2 i2 j end.
+
Fact col_mx_key :
unit.
+
Definition col_mx (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
'M[R]_(m1 + m2, n) :=
+
\matrix[col_mx_key]_(i, j)
+
match split i with inl i1 ⇒
A1 i1 j |
inr i2 ⇒
A2 i2 j end.
@@ -661,99 +665,99 @@ Type Definition*********************************
-
Fact lsubmx_key :
unit.
-
Definition lsubmx (
A :
'M[R]_(m, n1 + n2)) :=
-
\matrix[lsubmx_key]_(i, j) A i (
lshift n2 j).
+
Fact lsubmx_key :
unit.
+
Definition lsubmx (
A :
'M[R]_(m, n1 + n2)) :=
+
\matrix[lsubmx_key]_(i, j) A i (
lshift n2 j).
-
Fact rsubmx_key :
unit.
-
Definition rsubmx (
A :
'M[R]_(m, n1 + n2)) :=
-
\matrix[rsubmx_key]_(i, j) A i (
rshift n1 j).
+
Fact rsubmx_key :
unit.
+
Definition rsubmx (
A :
'M[R]_(m, n1 + n2)) :=
+
\matrix[rsubmx_key]_(i, j) A i (
rshift n1 j).
-
Fact usubmx_key :
unit.
-
Definition usubmx (
A :
'M[R]_(m1 + m2, n)) :=
-
\matrix[usubmx_key]_(i, j) A (
lshift m2 i)
j.
+
Fact usubmx_key :
unit.
+
Definition usubmx (
A :
'M[R]_(m1 + m2, n)) :=
+
\matrix[usubmx_key]_(i, j) A (
lshift m2 i)
j.
-
Fact dsubmx_key :
unit.
-
Definition dsubmx (
A :
'M[R]_(m1 + m2, n)) :=
-
\matrix[dsubmx_key]_(i, j) A (
rshift m1 i)
j.
+
Fact dsubmx_key :
unit.
+
Definition dsubmx (
A :
'M[R]_(m1 + m2, n)) :=
+
\matrix[dsubmx_key]_(i, j) A (
rshift m1 i)
j.
-
Lemma row_mxEl A1 A2 i j :
row_mx A1 A2 i (
lshift n2 j)
= A1 i j.
+
Lemma row_mxEl A1 A2 i j :
row_mx A1 A2 i (
lshift n2 j)
= A1 i j.
-
Lemma row_mxKl A1 A2 :
lsubmx (
row_mx A1 A2)
= A1.
+
Lemma row_mxKl A1 A2 :
lsubmx (
row_mx A1 A2)
= A1.
-
Lemma row_mxEr A1 A2 i j :
row_mx A1 A2 i (
rshift n1 j)
= A2 i j.
+
Lemma row_mxEr A1 A2 i j :
row_mx A1 A2 i (
rshift n1 j)
= A2 i j.
-
Lemma row_mxKr A1 A2 :
rsubmx (
row_mx A1 A2)
= A2.
+
Lemma row_mxKr A1 A2 :
rsubmx (
row_mx A1 A2)
= A2.
-
Lemma hsubmxK A :
row_mx (
lsubmx A) (
rsubmx A)
= A.
+
Lemma hsubmxK A :
row_mx (
lsubmx A) (
rsubmx A)
= A.
-
Lemma col_mxEu A1 A2 i j :
col_mx A1 A2 (
lshift m2 i)
j = A1 i j.
+
Lemma col_mxEu A1 A2 i j :
col_mx A1 A2 (
lshift m2 i)
j = A1 i j.
-
Lemma col_mxKu A1 A2 :
usubmx (
col_mx A1 A2)
= A1.
+
Lemma col_mxKu A1 A2 :
usubmx (
col_mx A1 A2)
= A1.
-
Lemma col_mxEd A1 A2 i j :
col_mx A1 A2 (
rshift m1 i)
j = A2 i j.
+
Lemma col_mxEd A1 A2 i j :
col_mx A1 A2 (
rshift m1 i)
j = A2 i j.
-
Lemma col_mxKd A1 A2 :
dsubmx (
col_mx A1 A2)
= A2.
+
Lemma col_mxKd A1 A2 :
dsubmx (
col_mx A1 A2)
= A2.
-
Lemma eq_row_mx A1 A2 B1 B2 :
row_mx A1 A2 = row_mx B1 B2 → A1 = B1 ∧ A2 = B2.
+
Lemma eq_row_mx A1 A2 B1 B2 :
row_mx A1 A2 = row_mx B1 B2 → A1 = B1 ∧ A2 = B2.
-
Lemma eq_col_mx A1 A2 B1 B2 :
col_mx A1 A2 = col_mx B1 B2 → A1 = B1 ∧ A2 = B2.
+
Lemma eq_col_mx A1 A2 B1 B2 :
col_mx A1 A2 = col_mx B1 B2 → A1 = B1 ∧ A2 = B2.
-
Lemma row_mx_const a :
row_mx (
const_mx a) (
const_mx a)
= const_mx a.
+
Lemma row_mx_const a :
row_mx (
const_mx a) (
const_mx a)
= const_mx a.
-
Lemma col_mx_const a :
col_mx (
const_mx a) (
const_mx a)
= const_mx a.
+
Lemma col_mx_const a :
col_mx (
const_mx a) (
const_mx a)
= const_mx a.
End CutPaste.
-
Lemma trmx_lsub m n1 n2 (
A :
'M_(m, n1 + n2)) :
(lsubmx A)^T = usubmx A^T.
+
Lemma trmx_lsub m n1 n2 (
A :
'M_(m, n1 + n2)) :
(lsubmx A)^T = usubmx A^T.
-
Lemma trmx_rsub m n1 n2 (
A :
'M_(m, n1 + n2)) :
(rsubmx A)^T = dsubmx A^T.
+
Lemma trmx_rsub m n1 n2 (
A :
'M_(m, n1 + n2)) :
(rsubmx A)^T = dsubmx A^T.
-
Lemma tr_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
(row_mx A1 A2)^T = col_mx A1^T A2^T.
+
Lemma tr_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
(row_mx A1 A2)^T = col_mx A1^T A2^T.
-
Lemma tr_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
(col_mx A1 A2)^T = row_mx A1^T A2^T.
+
Lemma tr_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
(col_mx A1 A2)^T = row_mx A1^T A2^T.
-
Lemma trmx_usub m1 m2 n (
A :
'M_(m1 + m2, n)) :
(usubmx A)^T = lsubmx A^T.
+
Lemma trmx_usub m1 m2 n (
A :
'M_(m1 + m2, n)) :
(usubmx A)^T = lsubmx A^T.
-
Lemma trmx_dsub m1 m2 n (
A :
'M_(m1 + m2, n)) :
(dsubmx A)^T = rsubmx A^T.
+
Lemma trmx_dsub m1 m2 n (
A :
'M_(m1 + m2, n)) :
(dsubmx A)^T = rsubmx A^T.
-
Lemma vsubmxK m1 m2 n (
A :
'M_(m1 + m2, n)) :
col_mx (
usubmx A) (
dsubmx A)
= A.
+
Lemma vsubmxK m1 m2 n (
A :
'M_(m1 + m2, n)) :
col_mx (
usubmx A) (
dsubmx A)
= A.
-
Lemma cast_row_mx m m' n1 n2 (
eq_m :
m = m')
A1 A2 :
-
castmx (eq_m, erefl _) (
row_mx A1 A2)
-
= row_mx (
castmx (eq_m, erefl n1) A1) (
castmx (eq_m, erefl n2) A2).
+
Lemma cast_row_mx m m' n1 n2 (
eq_m :
m = m')
A1 A2 :
+
castmx (eq_m, erefl _) (
row_mx A1 A2)
+
= row_mx (
castmx (eq_m, erefl n1) A1) (
castmx (eq_m, erefl n2) A2).
-
Lemma cast_col_mx m1 m2 n n' (
eq_n :
n = n')
A1 A2 :
-
castmx (erefl _, eq_n) (
col_mx A1 A2)
-
= col_mx (
castmx (erefl m1, eq_n) A1) (
castmx (erefl m2, eq_n) A2).
+
Lemma cast_col_mx m1 m2 n n' (
eq_n :
n = n')
A1 A2 :
+
castmx (erefl _, eq_n) (
col_mx A1 A2)
+
= col_mx (
castmx (erefl m1, eq_n) A1) (
castmx (erefl m2, eq_n) A2).
@@ -762,9 +766,9 @@ Type Definition*********************************
This lemma has Prenex Implicits to help RL rewrititng with castmx_sym.
-
Lemma row_mxA m n1 n2 n3 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) (
A3 :
'M_(m, n3)) :
-
let cast :=
(erefl m, esym (
addnA n1 n2 n3)
) in
-
row_mx A1 (
row_mx A2 A3)
= castmx cast (
row_mx (
row_mx A1 A2)
A3).
+
Lemma row_mxA m n1 n2 n3 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) (
A3 :
'M_(m, n3)) :
+
let cast :=
(erefl m, esym (
addnA n1 n2 n3)
) in
+
row_mx A1 (
row_mx A2 A3)
= castmx cast (
row_mx (
row_mx A1 A2)
A3).
Definition row_mxAx :=
row_mxA.
@@ -774,69 +778,69 @@ Type Definition*********************************
This lemma has Prenex Implicits to help RL rewrititng with castmx_sym.
-
Lemma col_mxA m1 m2 m3 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) (
A3 :
'M_(m3, n)) :
-
let cast :=
(esym (
addnA m1 m2 m3)
, erefl n) in
-
col_mx A1 (
col_mx A2 A3)
= castmx cast (
col_mx (
col_mx A1 A2)
A3).
+
Lemma col_mxA m1 m2 m3 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) (
A3 :
'M_(m3, n)) :
+
let cast :=
(esym (
addnA m1 m2 m3)
, erefl n) in
+
col_mx A1 (
col_mx A2 A3)
= castmx cast (
col_mx (
col_mx A1 A2)
A3).
Definition col_mxAx :=
col_mxA.
-
Lemma row_row_mx m n1 n2 i0 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
row i0 (
row_mx A1 A2)
= row_mx (
row i0 A1) (
row i0 A2).
+
Lemma row_row_mx m n1 n2 i0 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
row i0 (
row_mx A1 A2)
= row_mx (
row i0 A1) (
row i0 A2).
-
Lemma col_col_mx m1 m2 n j0 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
col j0 (
col_mx A1 A2)
= col_mx (
col j0 A1) (
col j0 A2).
+
Lemma col_col_mx m1 m2 n j0 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
col j0 (
col_mx A1 A2)
= col_mx (
col j0 A1) (
col j0 A2).
-
Lemma row'_row_mx m n1 n2 i0 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
row' i0 (
row_mx A1 A2)
= row_mx (
row' i0 A1) (
row' i0 A2).
+
Lemma row'_row_mx m n1 n2 i0 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
row' i0 (
row_mx A1 A2)
= row_mx (
row' i0 A1) (
row' i0 A2).
-
Lemma col'_col_mx m1 m2 n j0 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
col' j0 (
col_mx A1 A2)
= col_mx (
col' j0 A1) (
col' j0 A2).
+
Lemma col'_col_mx m1 m2 n j0 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
col' j0 (
col_mx A1 A2)
= col_mx (
col' j0 A1) (
col' j0 A2).
-
Lemma colKl m n1 n2 j1 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
col (
lshift n2 j1) (
row_mx A1 A2)
= col j1 A1.
+
Lemma colKl m n1 n2 j1 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
col (
lshift n2 j1) (
row_mx A1 A2)
= col j1 A1.
-
Lemma colKr m n1 n2 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
col (
rshift n1 j2) (
row_mx A1 A2)
= col j2 A2.
+
Lemma colKr m n1 n2 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
col (
rshift n1 j2) (
row_mx A1 A2)
= col j2 A2.
-
Lemma rowKu m1 m2 n i1 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
row (
lshift m2 i1) (
col_mx A1 A2)
= row i1 A1.
+
Lemma rowKu m1 m2 n i1 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
row (
lshift m2 i1) (
col_mx A1 A2)
= row i1 A1.
-
Lemma rowKd m1 m2 n i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
row (
rshift m1 i2) (
col_mx A1 A2)
= row i2 A2.
+
Lemma rowKd m1 m2 n i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
row (
rshift m1 i2) (
col_mx A1 A2)
= row i2 A2.
-
Lemma col'Kl m n1 n2 j1 (
A1 :
'M_(m, n1.+1)) (
A2 :
'M_(m, n2)) :
-
col' (
lshift n2 j1) (
row_mx A1 A2)
= row_mx (
col' j1 A1)
A2.
+
Lemma col'Kl m n1 n2 j1 (
A1 :
'M_(m, n1.+1)) (
A2 :
'M_(m, n2)) :
+
col' (
lshift n2 j1) (
row_mx A1 A2)
= row_mx (
col' j1 A1)
A2.
-
Lemma row'Ku m1 m2 n i1 (
A1 :
'M_(m1.+1, n)) (
A2 :
'M_(m2, n)) :
-
row' (
lshift m2 i1) (@
col_mx m1.+1 m2 n A1 A2)
= col_mx (
row' i1 A1)
A2.
+
Lemma row'Ku m1 m2 n i1 (
A1 :
'M_(m1.+1, n)) (
A2 :
'M_(m2, n)) :
+
row' (
lshift m2 i1) (@
col_mx m1.+1 m2 n A1 A2)
= col_mx (
row' i1 A1)
A2.
-
Lemma mx'_cast m n :
'I_n → (
m + n.-1)%
N = (m + n).-1.
+
Lemma mx'_cast m n :
'I_n → (
m + n.-1)%
N = (m + n).-1.
-
Lemma col'Kr m n1 n2 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
Lemma col'Kr m n1 n2 j2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
col' (
rshift n1 j2) (@
row_mx m n1 n2 A1 A2)
-
= castmx (erefl m, mx'_cast n1 j2) (
row_mx A1 (
col' j2 A2)).
+
= castmx (erefl m, mx'_cast n1 j2) (
row_mx A1 (
col' j2 A2)).
-
Lemma row'Kd m1 m2 n i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
Lemma row'Kd m1 m2 n i2 (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
row' (
rshift m1 i2) (
col_mx A1 A2)
-
= castmx (mx'_cast m1 i2, erefl n) (
col_mx A1 (
row' i2 A2)).
+
= castmx (mx'_cast m1 i2, erefl n) (
col_mx A1 (
row' i2 A2)).
Section Block.
-
Variables m1 m2 n1 n2 :
nat.
+
Variables m1 m2 n1 n2 :
nat.
-
Definition block_mx Aul Aur Adl Adr :
'M_(m1 + m2, n1 + n2) :=
+
Definition block_mx Aul Aur Adl Adr :
'M_(m1 + m2, n1 + n2) :=
col_mx (
row_mx Aul Aur) (
row_mx Adl Adr).
Lemma eq_block_mx Aul Aur Adl Adr Bul Bur Bdl Bdr :
-
block_mx Aul Aur Adl Adr = block_mx Bul Bur Bdl Bdr →
-
[/\ Aul = Bul, Aur = Bur, Adl = Bdl & Adr = Bdr].
+
block_mx Aul Aur Adl Adr = block_mx Bul Bur Bdl Bdr →
+
[/\ Aul = Bul, Aur = Bur, Adl = Bdl & Adr = Bdr].
Lemma block_mx_const a :
-
block_mx (
const_mx a) (
const_mx a) (
const_mx a) (
const_mx a)
= const_mx a.
+
block_mx (
const_mx a) (
const_mx a) (
const_mx a) (
const_mx a)
= const_mx a.
Section CutBlock.
-
Variable A :
matrix R (
m1 + m2) (
n1 + n2).
+
Variable A :
matrix R (
m1 + m2) (
n1 + n2).
Definition ulsubmx :=
lsubmx (
usubmx A).
@@ -873,7 +877,7 @@ Type Definition*********************************
Definition drsubmx :=
rsubmx (
dsubmx A).
-
Lemma submxK :
block_mx ulsubmx ursubmx dlsubmx drsubmx = A.
+
Lemma submxK :
block_mx ulsubmx ursubmx dlsubmx drsubmx = A.
End CutBlock.
@@ -882,30 +886,30 @@ Type Definition*********************************
Section CatBlock.
-
Variables (
Aul :
'M[R]_(m1, n1)) (
Aur :
'M[R]_(m1, n2)).
-
Variables (
Adl :
'M[R]_(m2, n1)) (
Adr :
'M[R]_(m2, n2)).
+
Variables (
Aul :
'M[R]_(m1, n1)) (
Aur :
'M[R]_(m1, n2)).
+
Variables (
Adl :
'M[R]_(m2, n1)) (
Adr :
'M[R]_(m2, n2)).
Let A :=
block_mx Aul Aur Adl Adr.
-
Lemma block_mxEul i j :
A (
lshift m2 i) (
lshift n2 j)
= Aul i j.
-
Lemma block_mxKul :
ulsubmx A = Aul.
+
Lemma block_mxEul i j :
A (
lshift m2 i) (
lshift n2 j)
= Aul i j.
+
Lemma block_mxKul :
ulsubmx A = Aul.
-
Lemma block_mxEur i j :
A (
lshift m2 i) (
rshift n1 j)
= Aur i j.
-
Lemma block_mxKur :
ursubmx A = Aur.
+
Lemma block_mxEur i j :
A (
lshift m2 i) (
rshift n1 j)
= Aur i j.
+
Lemma block_mxKur :
ursubmx A = Aur.
-
Lemma block_mxEdl i j :
A (
rshift m1 i) (
lshift n2 j)
= Adl i j.
-
Lemma block_mxKdl :
dlsubmx A = Adl.
+
Lemma block_mxEdl i j :
A (
rshift m1 i) (
lshift n2 j)
= Adl i j.
+
Lemma block_mxKdl :
dlsubmx A = Adl.
-
Lemma block_mxEdr i j :
A (
rshift m1 i) (
rshift n1 j)
= Adr i j.
-
Lemma block_mxKdr :
drsubmx A = Adr.
+
Lemma block_mxEdr i j :
A (
rshift m1 i) (
rshift n1 j)
= Adr i j.
+
Lemma block_mxKdr :
drsubmx A = Adr.
-
Lemma block_mxEv :
A = col_mx (
row_mx Aul Aur) (
row_mx Adl Adr).
+
Lemma block_mxEv :
A = col_mx (
row_mx Aul Aur) (
row_mx Adl Adr).
End CatBlock.
@@ -917,37 +921,37 @@ Type Definition*********************************
Section TrCutBlock.
-
Variables m1 m2 n1 n2 :
nat.
-
Variable A :
'M[R]_(m1 + m2, n1 + n2).
+
Variables m1 m2 n1 n2 :
nat.
+
Variable A :
'M[R]_(m1 + m2, n1 + n2).
-
Lemma trmx_ulsub :
(ulsubmx A)^T = ulsubmx A^T.
+
Lemma trmx_ulsub :
(ulsubmx A)^T = ulsubmx A^T.
-
Lemma trmx_ursub :
(ursubmx A)^T = dlsubmx A^T.
+
Lemma trmx_ursub :
(ursubmx A)^T = dlsubmx A^T.
-
Lemma trmx_dlsub :
(dlsubmx A)^T = ursubmx A^T.
+
Lemma trmx_dlsub :
(dlsubmx A)^T = ursubmx A^T.
-
Lemma trmx_drsub :
(drsubmx A)^T = drsubmx A^T.
+
Lemma trmx_drsub :
(drsubmx A)^T = drsubmx A^T.
End TrCutBlock.
Section TrBlock.
-
Variables m1 m2 n1 n2 :
nat.
-
Variables (
Aul :
'M[R]_(m1, n1)) (
Aur :
'M[R]_(m1, n2)).
-
Variables (
Adl :
'M[R]_(m2, n1)) (
Adr :
'M[R]_(m2, n2)).
+
Variables m1 m2 n1 n2 :
nat.
+
Variables (
Aul :
'M[R]_(m1, n1)) (
Aur :
'M[R]_(m1, n2)).
+
Variables (
Adl :
'M[R]_(m2, n1)) (
Adr :
'M[R]_(m2, n2)).
Lemma tr_block_mx :
-
(block_mx Aul Aur Adl Adr)^T = block_mx Aul^T Adl^T Aur^T Adr^T.
+
(block_mx Aul Aur Adl Adr)^T = block_mx Aul^T Adl^T Aur^T Adr^T.
Lemma block_mxEh :
-
block_mx Aul Aur Adl Adr = row_mx (
col_mx Aul Adl) (
col_mx Aur Adr).
+
block_mx Aul Aur Adl Adr = row_mx (
col_mx Aul Adl) (
col_mx Aur Adr).
End TrBlock.
@@ -958,14 +962,14 @@ Type Definition*********************************
Lemma block_mxA m1 m2 m3 n1 n2 n3
- (
A11 :
'M_(m1, n1)) (
A12 :
'M_(m1, n2)) (
A13 :
'M_(m1, n3))
- (
A21 :
'M_(m2, n1)) (
A22 :
'M_(m2, n2)) (
A23 :
'M_(m2, n3))
- (
A31 :
'M_(m3, n1)) (
A32 :
'M_(m3, n2)) (
A33 :
'M_(m3, n3)) :
-
let cast :=
(esym (
addnA m1 m2 m3)
, esym (
addnA n1 n2 n3)
) in
+ (
A11 :
'M_(m1, n1)) (
A12 :
'M_(m1, n2)) (
A13 :
'M_(m1, n3))
+ (
A21 :
'M_(m2, n1)) (
A22 :
'M_(m2, n2)) (
A23 :
'M_(m2, n3))
+ (
A31 :
'M_(m3, n1)) (
A32 :
'M_(m3, n2)) (
A33 :
'M_(m3, n3)) :
+
let cast :=
(esym (
addnA m1 m2 m3)
, esym (
addnA n1 n2 n3)
) in
let row1 :=
row_mx A12 A13 in let col1 :=
col_mx A21 A31 in
let row3 :=
row_mx A31 A32 in let col3 :=
col_mx A13 A23 in
block_mx A11 row1 col1 (
block_mx A22 A23 A32 A33)
-
= castmx cast (
block_mx (
block_mx A11 A12 A21 A22)
col3 row3 A33).
+
= castmx cast (
block_mx (
block_mx A11 A12 A21 A22)
col3 row3 A33).
Definition block_mxAx :=
block_mxA.
@@ -978,17 +982,17 @@ Type Definition*********************************
Section VecMatrix.
-
Variables m n :
nat.
+
Variables m n :
nat.
-
Lemma mxvec_cast :
#|{:'I_m × 'I_n}| = (
m × n)%
N.
+
Lemma mxvec_cast :
#|{:'I_m × 'I_n}| = (
m × n)%
N.
-
Definition mxvec_index (
i :
'I_m) (
j :
'I_n) :=
-
cast_ord mxvec_cast (
enum_rank (i, j)).
+
Definition mxvec_index (
i :
'I_m) (
j :
'I_n) :=
+
cast_ord mxvec_cast (
enum_rank (i, j)).
-
CoInductive is_mxvec_index :
'I_(m × n) → Type :=
+
Variant is_mxvec_index :
'I_(m × n) → Type :=
IsMxvecIndex i j :
is_mxvec_index (
mxvec_index i j).
@@ -996,28 +1000,28 @@ Type Definition*********************************
Coercion pair_of_mxvec_index k (
i_k :
is_mxvec_index k) :=
-
let:
IsMxvecIndex i j :=
i_k in (i, j).
+
let:
IsMxvecIndex i j :=
i_k in (i, j).
-
Definition mxvec (
A :
'M[R]_(m, n)) :=
-
castmx (erefl _, mxvec_cast) (
\row_k A (enum_val k).1 (enum_val k).2).
+
Definition mxvec (
A :
'M[R]_(m, n)) :=
+
castmx (erefl _, mxvec_cast) (
\row_k A (enum_val k).1 (enum_val k).2).
-
Fact vec_mx_key :
unit.
-
Definition vec_mx (
u :
'rV[R]_(m × n)) :=
-
\matrix[vec_mx_key]_(i, j) u 0 (
mxvec_index i j).
+
Fact vec_mx_key :
unit.
+
Definition vec_mx (
u :
'rV[R]_(m × n)) :=
+
\matrix[vec_mx_key]_(i, j) u 0 (
mxvec_index i j).
-
Lemma mxvecE A i j :
mxvec A 0 (
mxvec_index i j)
= A i j.
+
Lemma mxvecE A i j :
mxvec A 0 (
mxvec_index i j)
= A i j.
-
Lemma mxvecK :
cancel mxvec vec_mx.
+
Lemma mxvecK :
cancel mxvec vec_mx.
-
Lemma vec_mxK :
cancel vec_mx mxvec.
+
Lemma vec_mxK :
cancel vec_mx mxvec.
-
Lemma curry_mxvec_bij :
{on 'I_(m × n), bijective (prod_curry mxvec_index)}.
+
Lemma curry_mxvec_bij :
{on 'I_(m × n), bijective (prod_curry mxvec_index)}.
End VecMatrix.
@@ -1028,7 +1032,7 @@ Type Definition*********************************
-
Notation "A ^T" := (
trmx A) :
ring_scope.
+
Notation "A ^T" := (
trmx A) :
ring_scope.
@@ -1040,63 +1044,63 @@ Type Definition*********************************
Section MapMatrix.
-Variables (aT rT : Type) (f : aT → rT).
+Variables (aT rT : Type) (f : aT → rT).
-Fact map_mx_key : unit.
-Definition map_mx m n (A : 'M_(m, n)) := \matrix[map_mx_key]_(i, j) f (A i j).
+Fact map_mx_key : unit.
+Definition map_mx m n (A : 'M_(m, n)) := \matrix[map_mx_key]_(i, j) f (A i j).
-Notation "A ^f" := (map_mx A) : ring_scope.
+Notation "A ^f" := (map_mx A) : ring_scope.
Section OneMatrix.
-Variables (m n : nat) (A : 'M[aT]_(m, n)).
+Variables (m n : nat) (A : 'M[aT]_(m, n)).
-Lemma map_trmx : A^f^T = A^T^f.
+Lemma map_trmx : A^f^T = A^T^f.
-Lemma map_const_mx a : (const_mx a)^f = const_mx (f a) :> 'M_(m, n).
+Lemma map_const_mx a : (const_mx a)^f = const_mx (f a) :> 'M_(m, n).
-Lemma map_row i : (row i A)^f = row i A^f.
+Lemma map_row i : (row i A)^f = row i A^f.
-Lemma map_col j : (col j A)^f = col j A^f.
+Lemma map_col j : (col j A)^f = col j A^f.
-Lemma map_row' i0 : (row' i0 A)^f = row' i0 A^f.
+Lemma map_row' i0 : (row' i0 A)^f = row' i0 A^f.
-Lemma map_col' j0 : (col' j0 A)^f = col' j0 A^f.
+Lemma map_col' j0 : (col' j0 A)^f = col' j0 A^f.
-Lemma map_row_perm s : (row_perm s A)^f = row_perm s A^f.
+Lemma map_row_perm s : (row_perm s A)^f = row_perm s A^f.
-Lemma map_col_perm s : (col_perm s A)^f = col_perm s A^f.
+Lemma map_col_perm s : (col_perm s A)^f = col_perm s A^f.
-Lemma map_xrow i1 i2 : (xrow i1 i2 A)^f = xrow i1 i2 A^f.
+Lemma map_xrow i1 i2 : (xrow i1 i2 A)^f = xrow i1 i2 A^f.
-Lemma map_xcol j1 j2 : (xcol j1 j2 A)^f = xcol j1 j2 A^f.
+Lemma map_xcol j1 j2 : (xcol j1 j2 A)^f = xcol j1 j2 A^f.
-Lemma map_castmx m' n' c : (castmx c A)^f = castmx c A^f :> 'M_(m', n').
+Lemma map_castmx m' n' c : (castmx c A)^f = castmx c A^f :> 'M_(m', n').
-Lemma map_conform_mx m' n' (B : 'M_(m', n')) :
- (conform_mx B A)^f = conform_mx B^f A^f.
+Lemma map_conform_mx m' n' (B : 'M_(m', n')) :
+ (conform_mx B A)^f = conform_mx B^f A^f.
-Lemma map_mxvec : (mxvec A)^f = mxvec A^f.
+Lemma map_mxvec : (mxvec A)^f = mxvec A^f.
-Lemma map_vec_mx (v : 'rV_(m × n)) : (vec_mx v)^f = vec_mx v^f.
+Lemma map_vec_mx (v : 'rV_(m × n)) : (vec_mx v)^f = vec_mx v^f.
End OneMatrix.
@@ -1105,45 +1109,45 @@ Type Definition*********************************
Section Block.
-Variables m1 m2 n1 n2 : nat.
-Variables (Aul : 'M[aT]_(m1, n1)) (Aur : 'M[aT]_(m1, n2)).
-Variables (Adl : 'M[aT]_(m2, n1)) (Adr : 'M[aT]_(m2, n2)).
-Variables (Bh : 'M[aT]_(m1, n1 + n2)) (Bv : 'M[aT]_(m1 + m2, n1)).
-Variable B : 'M[aT]_(m1 + m2, n1 + n2).
+Variables m1 m2 n1 n2 : nat.
+Variables (Aul : 'M[aT]_(m1, n1)) (Aur : 'M[aT]_(m1, n2)).
+Variables (Adl : 'M[aT]_(m2, n1)) (Adr : 'M[aT]_(m2, n2)).
+Variables (Bh : 'M[aT]_(m1, n1 + n2)) (Bv : 'M[aT]_(m1 + m2, n1)).
+Variable B : 'M[aT]_(m1 + m2, n1 + n2).
-Lemma map_row_mx : (row_mx Aul Aur)^f = row_mx Aul^f Aur^f.
+Lemma map_row_mx : (row_mx Aul Aur)^f = row_mx Aul^f Aur^f.
-Lemma map_col_mx : (col_mx Aul Adl)^f = col_mx Aul^f Adl^f.
+Lemma map_col_mx : (col_mx Aul Adl)^f = col_mx Aul^f Adl^f.
Lemma map_block_mx :
- (block_mx Aul Aur Adl Adr)^f = block_mx Aul^f Aur^f Adl^f Adr^f.
+ (block_mx Aul Aur Adl Adr)^f = block_mx Aul^f Aur^f Adl^f Adr^f.
-Lemma map_lsubmx : (lsubmx Bh)^f = lsubmx Bh^f.
+Lemma map_lsubmx : (lsubmx Bh)^f = lsubmx Bh^f.
-Lemma map_rsubmx : (rsubmx Bh)^f = rsubmx Bh^f.
+Lemma map_rsubmx : (rsubmx Bh)^f = rsubmx Bh^f.
-Lemma map_usubmx : (usubmx Bv)^f = usubmx Bv^f.
+Lemma map_usubmx : (usubmx Bv)^f = usubmx Bv^f.
-Lemma map_dsubmx : (dsubmx Bv)^f = dsubmx Bv^f.
+Lemma map_dsubmx : (dsubmx Bv)^f = dsubmx Bv^f.
-Lemma map_ulsubmx : (ulsubmx B)^f = ulsubmx B^f.
+Lemma map_ulsubmx : (ulsubmx B)^f = ulsubmx B^f.
-Lemma map_ursubmx : (ursubmx B)^f = ursubmx B^f.
+Lemma map_ursubmx : (ursubmx B)^f = ursubmx B^f.
-Lemma map_dlsubmx : (dlsubmx B)^f = dlsubmx B^f.
+Lemma map_dlsubmx : (dlsubmx B)^f = dlsubmx B^f.
-Lemma map_drsubmx : (drsubmx B)^f = drsubmx B^f.
+Lemma map_drsubmx : (drsubmx B)^f = drsubmx B^f.
End Block.
@@ -1151,6 +1155,8 @@ Type Definition*********************************
End MapMatrix.
+
+
@@ -1169,14 +1175,14 @@ Type Definition*********************************
Section FixedDim.
-Variables m n : nat.
-Implicit Types A B : 'M[V]_(m, n).
+Variables m n : nat.
+Implicit Types A B : 'M[V]_(m, n).
-Fact oppmx_key : unit.
-Fact addmx_key : unit.
-Definition oppmx A := \matrix[oppmx_key]_(i, j) (- A i j).
-Definition addmx A B := \matrix[addmx_key]_(i, j) (A i j + B i j).
+Fact oppmx_key : unit.
+Fact addmx_key : unit.
+Definition oppmx A := \matrix[oppmx_key]_(i, j) (- A i j).
+Definition addmx A B := \matrix[addmx_key]_(i, j) (A i j + B i j).
@@ -1187,29 +1193,29 @@ Type Definition*********************************
-
Lemma addmxA :
associative addmx.
+
Lemma addmxA :
associative addmx.
-
Lemma addmxC :
commutative addmx.
+
Lemma addmxC :
commutative addmx.
-
Lemma add0mx :
left_id (
const_mx 0)
addmx.
+
Lemma add0mx :
left_id (
const_mx 0)
addmx.
-
Lemma addNmx :
left_inverse (
const_mx 0)
oppmx addmx.
+
Lemma addNmx :
left_inverse (
const_mx 0)
oppmx addmx.
Definition matrix_zmodMixin :=
ZmodMixin addmxA addmxC add0mx addNmx.
-
Canonical matrix_zmodType :=
Eval hnf in ZmodType 'M[V]_(m, n) matrix_zmodMixin.
+
Canonical matrix_zmodType :=
Eval hnf in ZmodType 'M[V]_(m, n) matrix_zmodMixin.
-
Lemma mulmxnE A d i j : (
A *+ d)
i j = A i j *+ d.
+
Lemma mulmxnE A d i j : (
A *+ d)
i j = A i j *+ d.
-
Lemma summxE I r (
P :
pred I) (
E :
I → 'M_(m, n))
i j :
- (
\sum_(k <- r | P k) E k)
i j = \sum_(k <- r | P k) E k i j.
+
Lemma summxE I r (
P :
pred I) (
E :
I → 'M_(m, n))
i j :
+ (
\sum_(k <- r | P k) E k)
i j = \sum_(k <- r | P k) E k i j.
Lemma const_mx_is_additive :
additive const_mx.
@@ -1222,11 +1228,11 @@ Type Definition*********************************
Section Additive.
-
Variables (
m n p q :
nat) (
f :
'I_p → 'I_q → 'I_m) (
g :
'I_p → 'I_q → 'I_n).
+
Variables (
m n p q :
nat) (
f :
'I_p → 'I_q → 'I_m) (
g :
'I_p → 'I_q → 'I_n).
-
Definition swizzle_mx k (
A :
'M[V]_(m, n)) :=
-
\matrix[k]_(i, j) A (
f i j) (
g i j).
+
Definition swizzle_mx k (
A :
'M[V]_(m, n)) :=
+
\matrix[k]_(i, j) A (
f i j) (
g i j).
Lemma swizzle_mx_is_additive k :
additive (
swizzle_mx k).
@@ -1256,96 +1262,96 @@ Type Definition*********************************
Additive (
can2_additive (@
vec_mxK V m n)
mxvecK).
-
Lemma flatmx0 n :
all_equal_to (0
: 'M_(0
, n)).
+
Lemma flatmx0 n :
all_equal_to (0
: 'M_(0
, n)).
-
Lemma thinmx0 n :
all_equal_to (0
: 'M_(n, 0
)).
+
Lemma thinmx0 n :
all_equal_to (0
: 'M_(n, 0
)).
-
Lemma trmx0 m n :
(0
: 'M_(m, n))^T = 0.
+
Lemma trmx0 m n :
(0
: 'M_(m, n))^T = 0.
-
Lemma row0 m n i0 :
row i0 (0
: 'M_(m, n))
= 0.
+
Lemma row0 m n i0 :
row i0 (0
: 'M_(m, n))
= 0.
-
Lemma col0 m n j0 :
col j0 (0
: 'M_(m, n))
= 0.
+
Lemma col0 m n j0 :
col j0 (0
: 'M_(m, n))
= 0.
-
Lemma mxvec_eq0 m n (
A :
'M_(m, n)) :
(mxvec A == 0
) = (A == 0
).
+
Lemma mxvec_eq0 m n (
A :
'M_(m, n)) :
(mxvec A == 0
) = (A == 0
).
-
Lemma vec_mx_eq0 m n (
v :
'rV_(m × n)) :
(vec_mx v == 0
) = (v == 0
).
+
Lemma vec_mx_eq0 m n (
v :
'rV_(m × n)) :
(vec_mx v == 0
) = (v == 0
).
-
Lemma row_mx0 m n1 n2 :
row_mx 0 0
= 0
:> 'M_(m, n1 + n2).
+
Lemma row_mx0 m n1 n2 :
row_mx 0 0
= 0
:> 'M_(m, n1 + n2).
-
Lemma col_mx0 m1 m2 n :
col_mx 0 0
= 0
:> 'M_(m1 + m2, n).
+
Lemma col_mx0 m1 m2 n :
col_mx 0 0
= 0
:> 'M_(m1 + m2, n).
-
Lemma block_mx0 m1 m2 n1 n2 :
block_mx 0 0 0 0
= 0
:> 'M_(m1 + m2, n1 + n2).
+
Lemma block_mx0 m1 m2 n1 n2 :
block_mx 0 0 0 0
= 0
:> 'M_(m1 + m2, n1 + n2).
Ltac split_mxE :=
apply/
matrixP⇒
i j;
do ![
rewrite mxE |
case:
split ⇒ ?].
-
Lemma opp_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
- row_mx A1 A2 = row_mx (
- A1) (
- A2).
+
Lemma opp_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
- row_mx A1 A2 = row_mx (
- A1) (
- A2).
-
Lemma opp_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
- col_mx A1 A2 = col_mx (
- A1) (
- A2).
+
Lemma opp_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
- col_mx A1 A2 = col_mx (
- A1) (
- A2).
-
Lemma opp_block_mx m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2)) :
-
- block_mx Aul Aur Adl Adr = block_mx (
- Aul) (
- Aur) (
- Adl) (
- Adr).
+
Lemma opp_block_mx m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2)) :
+
- block_mx Aul Aur Adl Adr = block_mx (
- Aul) (
- Aur) (
- Adl) (
- Adr).
-
Lemma add_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2))
B1 B2 :
-
row_mx A1 A2 + row_mx B1 B2 = row_mx (
A1 + B1) (
A2 + B2).
+
Lemma add_row_mx m n1 n2 (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2))
B1 B2 :
+
row_mx A1 A2 + row_mx B1 B2 = row_mx (
A1 + B1) (
A2 + B2).
-
Lemma add_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n))
B1 B2 :
-
col_mx A1 A2 + col_mx B1 B2 = col_mx (
A1 + B1) (
A2 + B2).
+
Lemma add_col_mx m1 m2 n (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n))
B1 B2 :
+
col_mx A1 A2 + col_mx B1 B2 = col_mx (
A1 + B1) (
A2 + B2).
-
Lemma add_block_mx m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2))
+
Lemma add_block_mx m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2))
Bul Bur Bdl Bdr :
let A :=
block_mx Aul Aur Adl Adr in let B :=
block_mx Bul Bur Bdl Bdr in
-
A + B = block_mx (
Aul + Bul) (
Aur + Bur) (
Adl + Bdl) (
Adr + Bdr).
+
A + B = block_mx (
Aul + Bul) (
Aur + Bur) (
Adl + Bdl) (
Adr + Bdr).
-
Lemma row_mx_eq0 (
m n1 n2 :
nat) (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)):
-
(row_mx A1 A2 == 0
) = (A1 == 0
) && (A2 == 0
).
+
Lemma row_mx_eq0 (
m n1 n2 :
nat) (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)):
+
(row_mx A1 A2 == 0
) = (A1 == 0
) && (A2 == 0
).
-
Lemma col_mx_eq0 (
m1 m2 n :
nat) (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)):
-
(col_mx A1 A2 == 0
) = (A1 == 0
) && (A2 == 0
).
-
+
Lemma col_mx_eq0 (
m1 m2 n :
nat) (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)):
+
(col_mx A1 A2 == 0
) = (A1 == 0
) && (A2 == 0
).
+
-
Lemma block_mx_eq0 m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2)) :
-
(block_mx Aul Aur Adl Adr == 0
) =
-
[&& Aul == 0
, Aur == 0
, Adl == 0
& Adr == 0
].
+
Lemma block_mx_eq0 m1 m2 n1 n2 (
Aul :
'M_(m1, n1))
Aur Adl (
Adr :
'M_(m2, n2)) :
+
(block_mx Aul Aur Adl Adr == 0
) =
+
[&& Aul == 0
, Aur == 0
, Adl == 0
& Adr == 0
].
-
Definition nz_row m n (
A :
'M_(m, n)) :=
-
oapp (
fun i ⇒
row i A) 0
[pick i | row i A != 0
].
+
Definition nz_row m n (
A :
'M_(m, n)) :=
+
oapp (
fun i ⇒
row i A) 0
[pick i | row i A != 0
].
-
Lemma nz_row_eq0 m n (
A :
'M_(m, n)) :
(nz_row A == 0
) = (A == 0
).
+
Lemma nz_row_eq0 m n (
A :
'M_(m, n)) :
(nz_row A == 0
) = (A == 0
).
End MatrixZmodule.
Section FinZmodMatrix.
-
Variables (
V :
finZmodType) (
m n :
nat).
+
Variables (
V :
finZmodType) (
m n :
nat).
-
Canonical matrix_finZmodType :=
Eval hnf in [finZmodType of MV].
+
Canonical matrix_finZmodType :=
Eval hnf in [finZmodType of MV].
Canonical matrix_baseFinGroupType :=
-
Eval hnf in [baseFinGroupType of MV for +%R].
-
Canonical matrix_finGroupType :=
Eval hnf in [finGroupType of MV for +%R].
+
Eval hnf in [baseFinGroupType of MV for +%R].
+
Canonical matrix_finGroupType :=
Eval hnf in [finGroupType of MV for +%R].
End FinZmodMatrix.
@@ -1358,20 +1364,20 @@ Type Definition*********************************
Section MapZmodMatrix.
-
Variables (
aR rR :
zmodType) (
f :
{additive aR → rR}) (
m n :
nat).
-
Implicit Type A :
'M[aR]_(m, n).
+
Variables (
aR rR :
zmodType) (
f :
{additive aR → rR}) (
m n :
nat).
+
Implicit Type A :
'M[aR]_(m, n).
-
Lemma map_mx0 : 0
^f = 0
:> 'M_(m, n).
+
Lemma map_mx0 : 0
^f = 0
:> 'M_(m, n).
-
Lemma map_mxN A :
(- A)^f = - A^f.
+
Lemma map_mxN A :
(- A)^f = - A^f.
-
Lemma map_mxD A B :
(A + B)^f = A^f + B^f.
+
Lemma map_mxD A B :
(A + B)^f = A^f + B^f.
-
Lemma map_mx_sub A B :
(A - B)^f = A^f - B^f.
+
Lemma map_mx_sub A B :
(A - B)^f = A^f - B^f.
Definition map_mx_sum :=
big_morph _ map_mxD map_mx0.
@@ -1408,12 +1414,12 @@ Type Definition*********************************
@@ -1422,23 +1428,23 @@ Type Definition*********************************
Basis
-
Fact delta_mx_key :
unit.
-
Definition delta_mx i0 j0 :
'M[R]_(m, n) :=
-
\matrix[delta_mx_key]_(i, j) ((i == i0) && (j == j0))%:R.
+
Fact delta_mx_key :
unit.
+
Definition delta_mx i0 j0 :
'M[R]_(m, n) :=
+
\matrix[delta_mx_key]_(i, j) ((i == i0) && (j == j0))%:R.
-
Lemma scale1mx A : 1
×m: A = A.
+
Lemma scale1mx A : 1
×m: A = A.
-
Lemma scalemxDl A x y :
(x + y) ×m: A = x ×m: A + y ×m: A.
+
Lemma scalemxDl A x y :
(x + y) ×m: A = x ×m: A + y ×m: A.
-
Lemma scalemxDr x A B :
x ×m: (A + B) = x ×m: A + x ×m: B.
+
Lemma scalemxDr x A B :
x ×m: (A + B) = x ×m: A + x ×m: B.
-
Lemma scalemxA x y A :
x ×m: (y ×m: A) = (x × y) ×m: A.
+
Lemma scalemxA x y A :
x ×m: (y ×m: A) = (x × y) ×m: A.
Definition matrix_lmodMixin :=
@@ -1446,14 +1452,14 @@ Type Definition*********************************
Canonical matrix_lmodType :=
-
Eval hnf in LmodType R 'M[R]_(m, n) matrix_lmodMixin.
+
Eval hnf in LmodType R 'M[R]_(m, n) matrix_lmodMixin.
-
Lemma scalemx_const a b :
a *: const_mx b = const_mx (
a × b).
+
Lemma scalemx_const a b :
a *: const_mx b = const_mx (
a × b).
Lemma matrix_sum_delta A :
-
A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j.
+
A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j.
End RingModule.
@@ -1491,51 +1497,51 @@ Type Definition*********************************
End StructuralLinear.
-
Lemma trmx_delta m n i j :
(delta_mx i j)^T = delta_mx j i :> 'M[R]_(n, m).
+
Lemma trmx_delta m n i j :
(delta_mx i j)^T = delta_mx j i :> 'M[R]_(n, m).
-
Lemma row_sum_delta n (
u :
'rV_n) :
u = \sum_(j < n) u 0
j *: delta_mx 0
j.
+
Lemma row_sum_delta n (
u :
'rV_n) :
u = \sum_(j < n) u 0
j *: delta_mx 0
j.
Lemma delta_mx_lshift m n1 n2 i j :
-
delta_mx i (
lshift n2 j)
= row_mx (
delta_mx i j) 0
:> 'M_(m, n1 + n2).
+
delta_mx i (
lshift n2 j)
= row_mx (
delta_mx i j) 0
:> 'M_(m, n1 + n2).
Lemma delta_mx_rshift m n1 n2 i j :
-
delta_mx i (
rshift n1 j)
= row_mx 0 (
delta_mx i j)
:> 'M_(m, n1 + n2).
+
delta_mx i (
rshift n1 j)
= row_mx 0 (
delta_mx i j)
:> 'M_(m, n1 + n2).
Lemma delta_mx_ushift m1 m2 n i j :
-
delta_mx (
lshift m2 i)
j = col_mx (
delta_mx i j) 0
:> 'M_(m1 + m2, n).
+
delta_mx (
lshift m2 i)
j = col_mx (
delta_mx i j) 0
:> 'M_(m1 + m2, n).
Lemma delta_mx_dshift m1 m2 n i j :
-
delta_mx (
rshift m1 i)
j = col_mx 0 (
delta_mx i j)
:> 'M_(m1 + m2, n).
+
delta_mx (
rshift m1 i)
j = col_mx 0 (
delta_mx i j)
:> 'M_(m1 + m2, n).
Lemma vec_mx_delta m n i j :
-
vec_mx (
delta_mx 0 (
mxvec_index i j))
= delta_mx i j :> 'M_(m, n).
+
vec_mx (
delta_mx 0 (
mxvec_index i j))
= delta_mx i j :> 'M_(m, n).
Lemma mxvec_delta m n i j :
-
mxvec (
delta_mx i j)
= delta_mx 0 (
mxvec_index i j)
:> 'rV_(m × n).
+
mxvec (
delta_mx i j)
= delta_mx 0 (
mxvec_index i j)
:> 'rV_(m × n).
Ltac split_mxE :=
apply/
matrixP⇒
i j;
do ![
rewrite mxE |
case:
split ⇒ ?].
-
Lemma scale_row_mx m n1 n2 a (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
-
a *: row_mx A1 A2 = row_mx (
a *: A1) (
a *: A2).
+
Lemma scale_row_mx m n1 n2 a (
A1 :
'M_(m, n1)) (
A2 :
'M_(m, n2)) :
+
a *: row_mx A1 A2 = row_mx (
a *: A1) (
a *: A2).
-
Lemma scale_col_mx m1 m2 n a (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
-
a *: col_mx A1 A2 = col_mx (
a *: A1) (
a *: A2).
+
Lemma scale_col_mx m1 m2 n a (
A1 :
'M_(m1, n)) (
A2 :
'M_(m2, n)) :
+
a *: col_mx A1 A2 = col_mx (
a *: A1) (
a *: A2).
-
Lemma scale_block_mx m1 m2 n1 n2 a (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
- (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2)) :
-
a *: block_mx Aul Aur Adl Adr
-
= block_mx (
a *: Aul) (
a *: Aur) (
a *: Adl) (
a *: Adr).
+
Lemma scale_block_mx m1 m2 n1 n2 a (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
+ (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2)) :
+
a *: block_mx Aul Aur Adl Adr
+
= block_mx (
a *: Aul) (
a *: Aur) (
a *: Adl) (
a *: Adr).
@@ -1546,12 +1552,12 @@ Type Definition*********************************
@@ -1572,51 +1578,51 @@ Type Definition*********************************
Section ScalarMx.
-
Variable n :
nat.
+
Variable n :
nat.
-
Fact scalar_mx_key :
unit.
-
Definition scalar_mx x :
'M[R]_n :=
-
\matrix[scalar_mx_key]_(i , j) (x *+ (i == j)).
-
Notation "x %:M" := (
scalar_mx x) :
ring_scope.
+
Fact scalar_mx_key :
unit.
+
Definition scalar_mx x :
'M[R]_n :=
+
\matrix[scalar_mx_key]_(i , j) (x *+ (i == j)).
+
Notation "x %:M" := (
scalar_mx x) :
ring_scope.
-
Lemma diag_const_mx a :
diag_mx (
const_mx a)
= a%:M :> 'M_n.
+
Lemma diag_const_mx a :
diag_mx (
const_mx a)
= a%:M :> 'M_n.
-
Lemma tr_scalar_mx a :
(a%:M)^T = a%:M.
+
Lemma tr_scalar_mx a :
(a%:M)^T = a%:M.
-
Lemma trmx1 :
(1
%:M)^T = 1
%:M.
+
Lemma trmx1 :
(1
%:M)^T = 1
%:M.
Lemma scalar_mx_is_additive :
additive scalar_mx.
Canonical scalar_mx_additive :=
Additive scalar_mx_is_additive.
-
Lemma scale_scalar_mx a1 a2 :
a1 *: a2%:M = (a1 × a2)%:M :> 'M_n.
+
Lemma scale_scalar_mx a1 a2 :
a1 *: a2%:M = (a1 × a2)%:M :> 'M_n.
-
Lemma scalemx1 a :
a *: 1
%:M = a%:M.
+
Lemma scalemx1 a :
a *: 1
%:M = a%:M.
-
Lemma scalar_mx_sum_delta a :
a%:M = \sum_i a *: delta_mx i i.
+
Lemma scalar_mx_sum_delta a :
a%:M = \sum_i a *: delta_mx i i.
-
Lemma mx1_sum_delta : 1
%:M = \sum_i delta_mx i i.
+
Lemma mx1_sum_delta : 1
%:M = \sum_i delta_mx i i.
-
Lemma row1 i :
row i 1
%:M = delta_mx 0
i.
+
Lemma row1 i :
row i 1
%:M = delta_mx 0
i.
-
Definition is_scalar_mx (
A :
'M[R]_n) :=
-
if insub 0%
N is Some i then A == (A i i)%:M else true.
+
Definition is_scalar_mx (
A :
'M[R]_n) :=
+
if insub 0%
N is Some i then A == (A i i)%:M else true.
-
Lemma is_scalar_mxP A :
reflect (
∃ a, A = a%:M) (
is_scalar_mx A).
+
Lemma is_scalar_mxP A :
reflect (
∃ a, A = a%:M) (
is_scalar_mx A).
-
Lemma scalar_mx_is_scalar a :
is_scalar_mx a%:M.
+
Lemma scalar_mx_is_scalar a :
is_scalar_mx a%:M.
Lemma mx0_is_scalar :
is_scalar_mx 0.
@@ -1625,13 +1631,13 @@ Type Definition*********************************
End ScalarMx.
-
Notation "x %:M" := (
scalar_mx _ x) :
ring_scope.
+
Notation "x %:M" := (
scalar_mx _ x) :
ring_scope.
-
Lemma mx11_scalar (
A :
'M_1) :
A = (A 0 0
)%:M.
+
Lemma mx11_scalar (
A :
'M_1) :
A = (A 0 0
)%:M.
-
Lemma scalar_mx_block n1 n2 a :
a%:M = block_mx a%:M 0 0
a%:M :> 'M_(n1 + n2).
+
Lemma scalar_mx_block n1 n2 a :
a%:M = block_mx a%:M 0 0
a%:M :> 'M_(n1 + n2).
-
Fact mulmx_key :
unit.
-
Definition mulmx {
m n p} (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
'M[R]_(m, p) :=
-
\matrix[mulmx_key]_(i, k) \sum_j (A i j × B j k).
+
Fact mulmx_key :
unit.
+
Definition mulmx {
m n p} (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
'M[R]_(m, p) :=
+
\matrix[mulmx_key]_(i, k) \sum_j (A i j × B j k).
-
Lemma mulmxA m n p q (
A :
'M_(m, n)) (
B :
'M_(n, p)) (
C :
'M_(p, q)) :
-
A ×m (B ×m C) = A ×m B ×m C.
+
Lemma mulmxA m n p q (
A :
'M_(m, n)) (
B :
'M_(n, p)) (
C :
'M_(p, q)) :
+
A ×m (B ×m C) = A ×m B ×m C.
-
Lemma mul0mx m n p (
A :
'M_(n, p)) : 0
×m A = 0
:> 'M_(m, p).
+
Lemma mul0mx m n p (
A :
'M_(n, p)) : 0
×m A = 0
:> 'M_(m, p).
-
Lemma mulmx0 m n p (
A :
'M_(m, n)) :
A ×m 0
= 0
:> 'M_(m, p).
+
Lemma mulmx0 m n p (
A :
'M_(m, n)) :
A ×m 0
= 0
:> 'M_(m, p).
-
Lemma mulmxN m n p (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
A ×m (- B) = - (A ×m B).
+
Lemma mulmxN m n p (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
A ×m (- B) = - (A ×m B).
-
Lemma mulNmx m n p (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
- A ×m B = - (A ×m B).
+
Lemma mulNmx m n p (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
- A ×m B = - (A ×m B).
-
Lemma mulmxDl m n p (
A1 A2 :
'M_(m, n)) (
B :
'M_(n, p)) :
-
(A1 + A2) ×m B = A1 ×m B + A2 ×m B.
+
Lemma mulmxDl m n p (
A1 A2 :
'M_(m, n)) (
B :
'M_(n, p)) :
+
(A1 + A2) ×m B = A1 ×m B + A2 ×m B.
-
Lemma mulmxDr m n p (
A :
'M_(m, n)) (
B1 B2 :
'M_(n, p)) :
-
A ×m (B1 + B2) = A ×m B1 + A ×m B2.
+
Lemma mulmxDr m n p (
A :
'M_(m, n)) (
B1 B2 :
'M_(n, p)) :
+
A ×m (B1 + B2) = A ×m B1 + A ×m B2.
-
Lemma mulmxBl m n p (
A1 A2 :
'M_(m, n)) (
B :
'M_(n, p)) :
-
(A1 - A2) ×m B = A1 ×m B - A2 ×m B.
+
Lemma mulmxBl m n p (
A1 A2 :
'M_(m, n)) (
B :
'M_(n, p)) :
+
(A1 - A2) ×m B = A1 ×m B - A2 ×m B.
-
Lemma mulmxBr m n p (
A :
'M_(m, n)) (
B1 B2 :
'M_(n, p)) :
-
A ×m (B1 - B2) = A ×m B1 - A ×m B2.
+
Lemma mulmxBr m n p (
A :
'M_(m, n)) (
B1 B2 :
'M_(n, p)) :
+
A ×m (B1 - B2) = A ×m B1 - A ×m B2.
-
Lemma mulmx_suml m n p (
A :
'M_(n, p))
I r P (
B_ :
I → 'M_(m, n)) :
-
(\sum_(i <- r | P i) B_ i) ×m A = \sum_(i <- r | P i) B_ i ×m A.
+
Lemma mulmx_suml m n p (
A :
'M_(n, p))
I r P (
B_ :
I → 'M_(m, n)) :
+
(\sum_(i <- r | P i) B_ i) ×m A = \sum_(i <- r | P i) B_ i ×m A.
-
Lemma mulmx_sumr m n p (
A :
'M_(m, n))
I r P (
B_ :
I → 'M_(n, p)) :
-
A ×m (\sum_(i <- r | P i) B_ i) = \sum_(i <- r | P i) A ×m B_ i.
+
Lemma mulmx_sumr m n p (
A :
'M_(m, n))
I r P (
B_ :
I → 'M_(n, p)) :
+
A ×m (\sum_(i <- r | P i) B_ i) = \sum_(i <- r | P i) A ×m B_ i.
-
Lemma scalemxAl m n p a (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
-
a *: (A ×m B) = (a *: A) ×m B.
+
Lemma scalemxAl m n p a (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
+
a *: (A ×m B) = (a *: A) ×m B.
@@ -1697,63 +1703,63 @@ Type Definition*********************************
-
Lemma rowE m n i (
A :
'M_(m, n)) :
row i A = delta_mx 0
i ×m A.
+
Lemma rowE m n i (
A :
'M_(m, n)) :
row i A = delta_mx 0
i ×m A.
-
Lemma row_mul m n p (
i :
'I_m)
A (
B :
'M_(n, p)) :
-
row i (
A ×m B)
= row i A ×m B.
+
Lemma row_mul m n p (
i :
'I_m)
A (
B :
'M_(n, p)) :
+
row i (
A ×m B)
= row i A ×m B.
-
Lemma mulmx_sum_row m n (
u :
'rV_m) (
A :
'M_(m, n)) :
-
u ×m A = \sum_i u 0
i *: row i A.
+
Lemma mulmx_sum_row m n (
u :
'rV_m) (
A :
'M_(m, n)) :
+
u ×m A = \sum_i u 0
i *: row i A.
-
Lemma mul_delta_mx_cond m n p (
j1 j2 :
'I_n) (
i1 :
'I_m) (
k2 :
'I_p) :
-
delta_mx i1 j1 ×m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2).
+
Lemma mul_delta_mx_cond m n p (
j1 j2 :
'I_n) (
i1 :
'I_m) (
k2 :
'I_p) :
+
delta_mx i1 j1 ×m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2).
-
Lemma mul_delta_mx m n p (
j :
'I_n) (
i :
'I_m) (
k :
'I_p) :
-
delta_mx i j ×m delta_mx j k = delta_mx i k.
+
Lemma mul_delta_mx m n p (
j :
'I_n) (
i :
'I_m) (
k :
'I_p) :
+
delta_mx i j ×m delta_mx j k = delta_mx i k.
-
Lemma mul_delta_mx_0 m n p (
j1 j2 :
'I_n) (
i1 :
'I_m) (
k2 :
'I_p) :
-
j1 != j2 → delta_mx i1 j1 ×m delta_mx j2 k2 = 0.
+
Lemma mul_delta_mx_0 m n p (
j1 j2 :
'I_n) (
i1 :
'I_m) (
k2 :
'I_p) :
+
j1 != j2 → delta_mx i1 j1 ×m delta_mx j2 k2 = 0.
-
Lemma mul_diag_mx m n d (
A :
'M_(m, n)) :
-
diag_mx d ×m A = \matrix_(i, j) (d 0
i × A i j).
+
Lemma mul_diag_mx m n d (
A :
'M_(m, n)) :
+
diag_mx d ×m A = \matrix_(i, j) (d 0
i × A i j).
-
Lemma mul_mx_diag m n (
A :
'M_(m, n))
d :
-
A ×m diag_mx d = \matrix_(i, j) (A i j × d 0
j).
+
Lemma mul_mx_diag m n (
A :
'M_(m, n))
d :
+
A ×m diag_mx d = \matrix_(i, j) (A i j × d 0
j).
-
Lemma mulmx_diag n (
d e :
'rV_n) :
-
diag_mx d ×m diag_mx e = diag_mx (
\row_j (d 0
j × e 0
j)).
+
Lemma mulmx_diag n (
d e :
'rV_n) :
+
diag_mx d ×m diag_mx e = diag_mx (
\row_j (d 0
j × e 0
j)).
-
Lemma mul_scalar_mx m n a (
A :
'M_(m, n)) :
a%:M ×m A = a *: A.
+
Lemma mul_scalar_mx m n a (
A :
'M_(m, n)) :
a%:M ×m A = a *: A.
-
Lemma scalar_mxM n a b :
(a × b)%:M = a%:M ×m b%:M :> 'M_n.
+
Lemma scalar_mxM n a b :
(a × b)%:M = a%:M ×m b%:M :> 'M_n.
-
Lemma mul1mx m n (
A :
'M_(m, n)) : 1
%:M ×m A = A.
+
Lemma mul1mx m n (
A :
'M_(m, n)) : 1
%:M ×m A = A.
-
Lemma mulmx1 m n (
A :
'M_(m, n)) :
A ×m 1
%:M = A.
+
Lemma mulmx1 m n (
A :
'M_(m, n)) :
A ×m 1
%:M = A.
-
Lemma mul_col_perm m n p s (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
-
col_perm s A ×m B = A ×m row_perm s^-1 B.
+
Lemma mul_col_perm m n p s (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
+
col_perm s A ×m B = A ×m row_perm s^-1 B.
-
Lemma mul_row_perm m n p s (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
-
A ×m row_perm s B = col_perm s^-1 A ×m B.
+
Lemma mul_row_perm m n p s (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
+
A ×m row_perm s B = col_perm s^-1 A ×m B.
-
Lemma mul_xcol m n p j1 j2 (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
-
xcol j1 j2 A ×m B = A ×m xrow j1 j2 B.
+
Lemma mul_xcol m n p j1 j2 (
A :
'M_(m, n)) (
B :
'M_(n, p)) :
+
xcol j1 j2 A ×m B = A ×m xrow j1 j2 B.
@@ -1764,58 +1770,58 @@ Type Definition*********************************
-
Definition perm_mx n s :
'M_n :=
row_perm s 1
%:M.
+
Definition perm_mx n s :
'M_n :=
row_perm s 1
%:M.
-
Definition tperm_mx n i1 i2 :
'M_n :=
perm_mx (
tperm i1 i2).
+
Definition tperm_mx n i1 i2 :
'M_n :=
perm_mx (
tperm i1 i2).
-
Lemma col_permE m n s (
A :
'M_(m, n)) :
col_perm s A = A ×m perm_mx s^-1.
+
Lemma col_permE m n s (
A :
'M_(m, n)) :
col_perm s A = A ×m perm_mx s^-1.
-
Lemma row_permE m n s (
A :
'M_(m, n)) :
row_perm s A = perm_mx s ×m A.
+
Lemma row_permE m n s (
A :
'M_(m, n)) :
row_perm s A = perm_mx s ×m A.
-
Lemma xcolE m n j1 j2 (
A :
'M_(m, n)) :
xcol j1 j2 A = A ×m tperm_mx j1 j2.
+
Lemma xcolE m n j1 j2 (
A :
'M_(m, n)) :
xcol j1 j2 A = A ×m tperm_mx j1 j2.
-
Lemma xrowE m n i1 i2 (
A :
'M_(m, n)) :
xrow i1 i2 A = tperm_mx i1 i2 ×m A.
+
Lemma xrowE m n i1 i2 (
A :
'M_(m, n)) :
xrow i1 i2 A = tperm_mx i1 i2 ×m A.
-
Lemma tr_perm_mx n (
s :
'S_n) :
(perm_mx s)^T = perm_mx s^-1.
+
Lemma tr_perm_mx n (
s :
'S_n) :
(perm_mx s)^T = perm_mx s^-1.
-
Lemma tr_tperm_mx n i1 i2 :
(tperm_mx i1 i2)^T = tperm_mx i1 i2 :> 'M_n.
+
Lemma tr_tperm_mx n i1 i2 :
(tperm_mx i1 i2)^T = tperm_mx i1 i2 :> 'M_n.
-
Lemma perm_mx1 n :
perm_mx 1
= 1
%:M :> 'M_n.
+
Lemma perm_mx1 n :
perm_mx 1
= 1
%:M :> 'M_n.
-
Lemma perm_mxM n (
s t :
'S_n) :
perm_mx (
s × t)
= perm_mx s ×m perm_mx t.
+
Lemma perm_mxM n (
s t :
'S_n) :
perm_mx (
s × t)
= perm_mx s ×m perm_mx t.
-
Definition is_perm_mx n (
A :
'M_n) :=
[∃ s, A == perm_mx s].
+
Definition is_perm_mx n (
A :
'M_n) :=
[∃ s, A == perm_mx s].
-
Lemma is_perm_mxP n (
A :
'M_n) :
-
reflect (
∃ s, A = perm_mx s) (
is_perm_mx A).
+
Lemma is_perm_mxP n (
A :
'M_n) :
+
reflect (
∃ s, A = perm_mx s) (
is_perm_mx A).
-
Lemma perm_mx_is_perm n (
s :
'S_n) :
is_perm_mx (
perm_mx s).
+
Lemma perm_mx_is_perm n (
s :
'S_n) :
is_perm_mx (
perm_mx s).
-
Lemma is_perm_mx1 n :
is_perm_mx (1
%:M : 'M_n).
+
Lemma is_perm_mx1 n :
is_perm_mx (1
%:M : 'M_n).
-
Lemma is_perm_mxMl n (
A B :
'M_n) :
-
is_perm_mx A → is_perm_mx (
A ×m B)
= is_perm_mx B.
+
Lemma is_perm_mxMl n (
A B :
'M_n) :
+
is_perm_mx A → is_perm_mx (
A ×m B)
= is_perm_mx B.
-
Lemma is_perm_mx_tr n (
A :
'M_n) :
is_perm_mx A^T = is_perm_mx A.
+
Lemma is_perm_mx_tr n (
A :
'M_n) :
is_perm_mx A^T = is_perm_mx A.
-
Lemma is_perm_mxMr n (
A B :
'M_n) :
-
is_perm_mx B → is_perm_mx (
A ×m B)
= is_perm_mx A.
+
Lemma is_perm_mxMr n (
A B :
'M_n) :
+
is_perm_mx B → is_perm_mx (
A ×m B)
= is_perm_mx A.
@@ -1826,56 +1832,56 @@ Type Definition*********************************
-
Fact pid_mx_key :
unit.
-
Definition pid_mx {
m n}
r :
'M[R]_(m, n) :=
-
\matrix[pid_mx_key]_(i, j) ((i == j :> nat) && (i < r))%:R.
+
Fact pid_mx_key :
unit.
+
Definition pid_mx {
m n}
r :
'M[R]_(m, n) :=
+
\matrix[pid_mx_key]_(i, j) ((i == j :> nat) && (i < r))%:R.
-
Lemma pid_mx_0 m n :
pid_mx 0
= 0
:> 'M_(m, n).
+
Lemma pid_mx_0 m n :
pid_mx 0
= 0
:> 'M_(m, n).
-
Lemma pid_mx_1 r :
pid_mx r = 1
%:M :> 'M_r.
+
Lemma pid_mx_1 r :
pid_mx r = 1
%:M :> 'M_r.
-
Lemma pid_mx_row n r :
pid_mx r = row_mx 1
%:M 0
:> 'M_(r, r + n).
+
Lemma pid_mx_row n r :
pid_mx r = row_mx 1
%:M 0
:> 'M_(r, r + n).
-
Lemma pid_mx_col m r :
pid_mx r = col_mx 1
%:M 0
:> 'M_(r + m, r).
+
Lemma pid_mx_col m r :
pid_mx r = col_mx 1
%:M 0
:> 'M_(r + m, r).
-
Lemma pid_mx_block m n r :
pid_mx r = block_mx 1
%:M 0 0 0
:> 'M_(r + m, r + n).
+
Lemma pid_mx_block m n r :
pid_mx r = block_mx 1
%:M 0 0 0
:> 'M_(r + m, r + n).
-
Lemma tr_pid_mx m n r :
(pid_mx r)^T = pid_mx r :> 'M_(n, m).
+
Lemma tr_pid_mx m n r :
(pid_mx r)^T = pid_mx r :> 'M_(n, m).
-
Lemma pid_mx_minv m n r :
pid_mx (
minn m r)
= pid_mx r :> 'M_(m, n).
+
Lemma pid_mx_minv m n r :
pid_mx (
minn m r)
= pid_mx r :> 'M_(m, n).
-
Lemma pid_mx_minh m n r :
pid_mx (
minn n r)
= pid_mx r :> 'M_(m, n).
+
Lemma pid_mx_minh m n r :
pid_mx (
minn n r)
= pid_mx r :> 'M_(m, n).
Lemma mul_pid_mx m n p q r :
-
(pid_mx q : 'M_(m, n)) ×m (pid_mx r : 'M_(n, p)) = pid_mx (
minn n (
minn q r)).
+
(pid_mx q : 'M_(m, n)) ×m (pid_mx r : 'M_(n, p)) = pid_mx (
minn n (
minn q r)).
Lemma pid_mx_id m n p r :
-
r ≤ n → (pid_mx r : 'M_(m, n)) ×m (pid_mx r : 'M_(n, p)) = pid_mx r.
+
r ≤ n → (pid_mx r : 'M_(m, n)) ×m (pid_mx r : 'M_(n, p)) = pid_mx r.
-
Definition copid_mx {
n}
r :
'M_n := 1
%:M - pid_mx r.
+
Definition copid_mx {
n}
r :
'M_n := 1
%:M - pid_mx r.
Lemma mul_copid_mx_pid m n r :
-
r ≤ m → copid_mx r ×m pid_mx r = 0
:> 'M_(m, n).
+
r ≤ m → copid_mx r ×m pid_mx r = 0
:> 'M_(m, n).
Lemma mul_pid_mx_copid m n r :
-
r ≤ n → pid_mx r ×m copid_mx r = 0
:> 'M_(m, n).
+
r ≤ n → pid_mx r ×m copid_mx r = 0
:> 'M_(m, n).
Lemma copid_mx_id n r :
-
r ≤ n → copid_mx r ×m copid_mx r = copid_mx r :> 'M_n.
+
r ≤ n → copid_mx r ×m copid_mx r = copid_mx r :> 'M_n.
@@ -1884,46 +1890,46 @@ Type Definition*********************************
Block products; we cover all 1 x 2, 2 x 1, and 2 x 2 block products.
-
Lemma mul_mx_row m n p1 p2 (
A :
'M_(m, n)) (
Bl :
'M_(n, p1)) (
Br :
'M_(n, p2)) :
-
A ×m row_mx Bl Br = row_mx (
A ×m Bl) (
A ×m Br).
+
Lemma mul_mx_row m n p1 p2 (
A :
'M_(m, n)) (
Bl :
'M_(n, p1)) (
Br :
'M_(n, p2)) :
+
A ×m row_mx Bl Br = row_mx (
A ×m Bl) (
A ×m Br).
-
Lemma mul_col_mx m1 m2 n p (
Au :
'M_(m1, n)) (
Ad :
'M_(m2, n)) (
B :
'M_(n, p)) :
-
col_mx Au Ad ×m B = col_mx (
Au ×m B) (
Ad ×m B).
+
Lemma mul_col_mx m1 m2 n p (
Au :
'M_(m1, n)) (
Ad :
'M_(m2, n)) (
B :
'M_(n, p)) :
+
col_mx Au Ad ×m B = col_mx (
Au ×m B) (
Ad ×m B).
-
Lemma mul_row_col m n1 n2 p (
Al :
'M_(m, n1)) (
Ar :
'M_(m, n2))
- (
Bu :
'M_(n1, p)) (
Bd :
'M_(n2, p)) :
-
row_mx Al Ar ×m col_mx Bu Bd = Al ×m Bu + Ar ×m Bd.
+
Lemma mul_row_col m n1 n2 p (
Al :
'M_(m, n1)) (
Ar :
'M_(m, n2))
+ (
Bu :
'M_(n1, p)) (
Bd :
'M_(n2, p)) :
+
row_mx Al Ar ×m col_mx Bu Bd = Al ×m Bu + Ar ×m Bd.
-
Lemma mul_col_row m1 m2 n p1 p2 (
Au :
'M_(m1, n)) (
Ad :
'M_(m2, n))
- (
Bl :
'M_(n, p1)) (
Br :
'M_(n, p2)) :
-
col_mx Au Ad ×m row_mx Bl Br
-
= block_mx (
Au ×m Bl) (
Au ×m Br) (
Ad ×m Bl) (
Ad ×m Br).
+
Lemma mul_col_row m1 m2 n p1 p2 (
Au :
'M_(m1, n)) (
Ad :
'M_(m2, n))
+ (
Bl :
'M_(n, p1)) (
Br :
'M_(n, p2)) :
+
col_mx Au Ad ×m row_mx Bl Br
+
= block_mx (
Au ×m Bl) (
Au ×m Br) (
Ad ×m Bl) (
Ad ×m Br).
-
Lemma mul_row_block m n1 n2 p1 p2 (
Al :
'M_(m, n1)) (
Ar :
'M_(m, n2))
- (
Bul :
'M_(n1, p1)) (
Bur :
'M_(n1, p2))
- (
Bdl :
'M_(n2, p1)) (
Bdr :
'M_(n2, p2)) :
-
row_mx Al Ar ×m block_mx Bul Bur Bdl Bdr
-
= row_mx (
Al ×m Bul + Ar ×m Bdl) (
Al ×m Bur + Ar ×m Bdr).
+
Lemma mul_row_block m n1 n2 p1 p2 (
Al :
'M_(m, n1)) (
Ar :
'M_(m, n2))
+ (
Bul :
'M_(n1, p1)) (
Bur :
'M_(n1, p2))
+ (
Bdl :
'M_(n2, p1)) (
Bdr :
'M_(n2, p2)) :
+
row_mx Al Ar ×m block_mx Bul Bur Bdl Bdr
+
= row_mx (
Al ×m Bul + Ar ×m Bdl) (
Al ×m Bur + Ar ×m Bdr).
-
Lemma mul_block_col m1 m2 n1 n2 p (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
- (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2))
- (
Bu :
'M_(n1, p)) (
Bd :
'M_(n2, p)) :
-
block_mx Aul Aur Adl Adr ×m col_mx Bu Bd
-
= col_mx (
Aul ×m Bu + Aur ×m Bd) (
Adl ×m Bu + Adr ×m Bd).
+
Lemma mul_block_col m1 m2 n1 n2 p (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
+ (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2))
+ (
Bu :
'M_(n1, p)) (
Bd :
'M_(n2, p)) :
+
block_mx Aul Aur Adl Adr ×m col_mx Bu Bd
+
= col_mx (
Aul ×m Bu + Aur ×m Bd) (
Adl ×m Bu + Adr ×m Bd).
-
Lemma mulmx_block m1 m2 n1 n2 p1 p2 (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
- (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2))
- (
Bul :
'M_(n1, p1)) (
Bur :
'M_(n1, p2))
- (
Bdl :
'M_(n2, p1)) (
Bdr :
'M_(n2, p2)) :
-
block_mx Aul Aur Adl Adr ×m block_mx Bul Bur Bdl Bdr
-
= block_mx (
Aul ×m Bul + Aur ×m Bdl) (
Aul ×m Bur + Aur ×m Bdr)
- (
Adl ×m Bul + Adr ×m Bdl) (
Adl ×m Bur + Adr ×m Bdr).
+
Lemma mulmx_block m1 m2 n1 n2 p1 p2 (
Aul :
'M_(m1, n1)) (
Aur :
'M_(m1, n2))
+ (
Adl :
'M_(m2, n1)) (
Adr :
'M_(m2, n2))
+ (
Bul :
'M_(n1, p1)) (
Bur :
'M_(n1, p2))
+ (
Bdl :
'M_(n2, p1)) (
Bdr :
'M_(n2, p2)) :
+
block_mx Aul Aur Adl Adr ×m block_mx Bul Bur Bdl Bdr
+
= block_mx (
Aul ×m Bul + Aur ×m Bdl) (
Aul ×m Bur + Aur ×m Bdr)
+ (
Adl ×m Bul + Adr ×m Bdl) (
Adl ×m Bur + Adr ×m Bdr).
-Variables m n : nat.
+Variables m n : nat.
-Fact lin1_mx_key : unit.
-Definition lin1_mx (f : 'rV[R]_m → 'rV[R]_n) :=
- \matrix[lin1_mx_key]_(i, j) f (delta_mx 0 i) 0 j.
+Fact lin1_mx_key : unit.
+Definition lin1_mx (f : 'rV[R]_m → 'rV[R]_n) :=
+ \matrix[lin1_mx_key]_(i, j) f (delta_mx 0 i) 0 j.
-Variable f : {linear 'rV[R]_m → 'rV[R]_n}.
+Variable f : {linear 'rV[R]_m → 'rV[R]_n}.
-Lemma mul_rV_lin1 u : u ×m lin1_mx f = f u.
+Lemma mul_rV_lin1 u : u ×m lin1_mx f = f u.
End LinRowVector.
@@ -1961,26 +1967,26 @@ Type Definition*********************************
Section LinMatrix.
-Variables m1 n1 m2 n2 : nat.
+Variables m1 n1 m2 n2 : nat.
-Definition lin_mx (f : 'M[R]_(m1, n1) → 'M[R]_(m2, n2)) :=
- lin1_mx (mxvec \o f \o vec_mx).
+Definition lin_mx (f : 'M[R]_(m1, n1) → 'M[R]_(m2, n2)) :=
+ lin1_mx (mxvec \o f \o vec_mx).
-Variable f : {linear 'M[R]_(m1, n1) → 'M[R]_(m2, n2)}.
+Variable f : {linear 'M[R]_(m1, n1) → 'M[R]_(m2, n2)}.
-Lemma mul_rV_lin u : u ×m lin_mx f = mxvec (f (vec_mx u)).
+Lemma mul_rV_lin u : u ×m lin_mx f = mxvec (f (vec_mx u)).
-Lemma mul_vec_lin A : mxvec A ×m lin_mx f = mxvec (f A).
+Lemma mul_vec_lin A : mxvec A ×m lin_mx f = mxvec (f A).
-Lemma mx_rV_lin u : vec_mx (u ×m lin_mx f) = f (vec_mx u).
+Lemma mx_rV_lin u : vec_mx (u ×m lin_mx f) = f (vec_mx u).
-Lemma mx_vec_lin A : vec_mx (mxvec A ×m lin_mx f) = f A.
+Lemma mx_vec_lin A : vec_mx (mxvec A ×m lin_mx f) = f A.
End LinMatrix.
@@ -1992,12 +1998,12 @@ Type Definition*********************************
Section Mulmxr.
-Variables m n p : nat.
-Implicit Type A : 'M[R]_(m, n).
-Implicit Type B : 'M[R]_(n, p).
+Variables m n p : nat.
+Implicit Type A : 'M[R]_(m, n).
+Implicit Type B : 'M[R]_(n, p).
-Definition mulmxr_head t B A := let: tt := t in A ×m B.
+Definition mulmxr_head t B A := let: tt := t in A ×m B.
Definition lin_mulmxr B := lin_mx (mulmxr B).
@@ -2025,13 +2031,13 @@ Type Definition*********************************
Section Trace.
-Variable n : nat.
+Variable n : nat.
-Definition mxtrace (A : 'M[R]_n) := \sum_i A i i.
+Definition mxtrace (A : 'M[R]_n) := \sum_i A i i.
-Lemma mxtrace_tr A : \tr A^T = \tr A.
+Lemma mxtrace_tr A : \tr A^T = \tr A.
Lemma mxtrace_is_scalar : scalar mxtrace.
@@ -2039,28 +2045,28 @@ Type Definition*********************************
Canonical mxtrace_linear := Linear mxtrace_is_scalar.
-Lemma mxtrace0 : \tr 0 = 0.
-Lemma mxtraceD A B : \tr (A + B) = \tr A + \tr B.
-Lemma mxtraceZ a A : \tr (a *: A) = a × \tr A.
+Lemma mxtrace0 : \tr 0 = 0.
+Lemma mxtraceD A B : \tr (A + B) = \tr A + \tr B.
+Lemma mxtraceZ a A : \tr (a *: A) = a × \tr A.
-Lemma mxtrace_diag D : \tr (diag_mx D) = \sum_j D 0 j.
+Lemma mxtrace_diag D : \tr (diag_mx D) = \sum_j D 0 j.
-Lemma mxtrace_scalar a : \tr a%:M = a *+ n.
+Lemma mxtrace_scalar a : \tr a%:M = a *+ n.
-Lemma mxtrace1 : \tr 1%:M = n%:R.
+Lemma mxtrace1 : \tr 1%:M = n%:R.
End Trace.
-Lemma trace_mx11 (A : 'M_1) : \tr A = A 0 0.
+Lemma trace_mx11 (A : 'M_1) : \tr A = A 0 0.
-Lemma mxtrace_block n1 n2 (Aul : 'M_n1) Aur Adl (Adr : 'M_n2) :
- \tr (block_mx Aul Aur Adl Adr) = \tr Aul + \tr Adr.
+Lemma mxtrace_block n1 n2 (Aul : 'M_n1) Aur Adl (Adr : 'M_n2) :
+ \tr (block_mx Aul Aur Adl Adr) = \tr Aul + \tr Adr.
@@ -2073,10 +2079,10 @@ Type Definition*********************************
Section MatrixRing.
-Variable n' : nat.
+Variable n' : nat.
-Lemma matrix_nonzero1 : 1%:M != 0 :> 'M_n.
+Lemma matrix_nonzero1 : 1%:M != 0 :> 'M_n.
Definition matrix_ringMixin :=
@@ -2084,12 +2090,12 @@ Type Definition*********************************
(@mulmxDl n n n) (@mulmxDr n n n) matrix_nonzero1.
-Canonical matrix_ringType := Eval hnf in RingType 'M[R]_n matrix_ringMixin.
-Canonical matrix_lAlgType := Eval hnf in LalgType R 'M[R]_n (@scalemxAl n n n).
+Canonical matrix_ringType := Eval hnf in RingType 'M[R]_n matrix_ringMixin.
+Canonical matrix_lAlgType := Eval hnf in LalgType R 'M[R]_n (@scalemxAl n n n).
-Lemma mulmxE : mulmx = *%R.
-Lemma idmxE : 1%:M = 1 :> 'M_n.
+Lemma mulmxE : mulmx = *%R.
+Lemma idmxE : 1%:M = 1 :> 'M_n.
Lemma scalar_mx_is_multiplicative : multiplicative (@scalar_mx n).
@@ -2110,7 +2116,7 @@ Type Definition*********************************
@@ -2121,20 +2127,20 @@ Type Definition*********************************
@@ -2145,10 +2151,10 @@ Type Definition*********************************
@@ -2178,8 +2184,8 @@ Type Definition*********************************
The cofactor of a matrix on the indexes i and j
@@ -2188,8 +2194,8 @@ Type Definition*********************************
The adjugate matrix : defined as the transpose of the matrix of cofactors
@@ -2213,16 +2219,20 @@ Type Definition*********************************
Non-commutative transpose requires multiplication in the converse ring.
-
Lemma trmx_mul_rev (
R :
ringType)
m n p (
A :
'M[R]_(m, n)) (
B :
'M[R]_(n, p)) :
-
(A ×m B)^T = (B : 'M[R^c]_(n, p))^T ×m (A : 'M[R^c]_(m, n))^T.
+
Lemma trmx_mul_rev (
R :
ringType)
m n p (
A :
'M[R]_(m, n)) (
B :
'M[R]_(n, p)) :
+
(A ×m B)^T = (B : 'M[R^c]_(n, p))^T ×m (A : 'M[R^c]_(m, n))^T.
+
Canonical matrix_countZmodType (
M :
countZmodType)
m n :=
+
[countZmodType of 'M[M]_(m, n)].
+
Canonical matrix_countRingType (
R :
countRingType)
n :=
+
[countRingType of 'M[R]_n.+1].
Canonical matrix_finLmodType (
R :
finRingType)
m n :=
-
[finLmodType R of 'M[R]_(m, n)].
+
[finLmodType R of 'M[R]_(m, n)].
Canonical matrix_finRingType (
R :
finRingType)
n' :=
-
Eval hnf in [finRingType of 'M[R]_n'.+1].
+
Eval hnf in [finRingType of 'M[R]_n'.+1].
Canonical matrix_finLalgType (
R :
finRingType)
n' :=
-
[finLalgType R of 'M[R]_n'.+1].
+
[finLalgType R of 'M[R]_n'.+1].
-Variables (aR rR : ringType) (f : {rmorphism aR → rR}).
+Variables (aR rR : ringType) (f : {rmorphism aR → rR}).
Section FixedSize.
-Variables m n p : nat.
-Implicit Type A : 'M[aR]_(m, n).
+Variables m n p : nat.
+Implicit Type A : 'M[aR]_(m, n).
-Lemma map_mxZ a A : (a *: A)^f = f a *: A^f.
+Lemma map_mxZ a A : (a *: A)^f = f a *: A^f.
-Lemma map_mxM A B : (A ×m B)^f = A^f ×m B^f :> 'M_(m, p).
+Lemma map_mxM A B : (A ×m B)^f = A^f ×m B^f :> 'M_(m, p).
-Lemma map_delta_mx i j : (delta_mx i j)^f = delta_mx i j :> 'M_(m, n).
+Lemma map_delta_mx i j : (delta_mx i j)^f = delta_mx i j :> 'M_(m, n).
-Lemma map_diag_mx d : (diag_mx d)^f = diag_mx d^f :> 'M_n.
+Lemma map_diag_mx d : (diag_mx d)^f = diag_mx d^f :> 'M_n.
-Lemma map_scalar_mx a : a%:M^f = (f a)%:M :> 'M_n.
+Lemma map_scalar_mx a : a%:M^f = (f a)%:M :> 'M_n.
-Lemma map_mx1 : 1%:M^f = 1%:M :> 'M_n.
+Lemma map_mx1 : 1%:M^f = 1%:M :> 'M_n.
-Lemma map_perm_mx (s : 'S_n) : (perm_mx s)^f = perm_mx s.
+Lemma map_perm_mx (s : 'S_n) : (perm_mx s)^f = perm_mx s.
-Lemma map_tperm_mx (i1 i2 : 'I_n) : (tperm_mx i1 i2)^f = tperm_mx i1 i2.
+Lemma map_tperm_mx (i1 i2 : 'I_n) : (tperm_mx i1 i2)^f = tperm_mx i1 i2.
-Lemma map_pid_mx r : (pid_mx r)^f = pid_mx r :> 'M_(m, n).
+Lemma map_pid_mx r : (pid_mx r)^f = pid_mx r :> 'M_(m, n).
-Lemma trace_map_mx (A : 'M_n) : \tr A^f = f (\tr A).
+Lemma trace_map_mx (A : 'M_n) : \tr A^f = f (\tr A).
-Lemma det_map_mx n' (A : 'M_n') : \det A^f = f (\det A).
+Lemma det_map_mx n' (A : 'M_n') : \det A^f = f (\det A).
-Lemma cofactor_map_mx (A : 'M_n) i j : cofactor A^f i j = f (cofactor A i j).
+Lemma cofactor_map_mx (A : 'M_n) i j : cofactor A^f i j = f (cofactor A i j).
-Lemma map_mx_adj (A : 'M_n) : (\adj A)^f = \adj A^f.
+Lemma map_mx_adj (A : 'M_n) : (\adj A)^f = \adj A^f.
End FixedSize.
-Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n.
+Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n.
-Lemma map_mx_is_multiplicative n' (n := n'.+1) :
- multiplicative ((map_mx f) n n).
+Lemma map_mx_is_multiplicative n' (n := n'.+1) :
+ multiplicative (map_mx f : 'M_n → 'M_n).
Canonical map_mx_rmorphism n' := AddRMorphism (map_mx_is_multiplicative n').
-Lemma map_lin1_mx m n (g : 'rV_m → 'rV_n) gf :
- (∀ v, (g v)^f = gf v^f) → (lin1_mx g)^f = lin1_mx gf.
+Lemma map_lin1_mx m n (g : 'rV_m → 'rV_n) gf :
+ (∀ v, (g v)^f = gf v^f) → (lin1_mx g)^f = lin1_mx gf.
-Lemma map_lin_mx m1 n1 m2 n2 (g : 'M_(m1, n1) → 'M_(m2, n2)) gf :
- (∀ A, (g A)^f = gf A^f) → (lin_mx g)^f = lin_mx gf.
+Lemma map_lin_mx m1 n1 m2 n2 (g : 'M_(m1, n1) → 'M_(m2, n2)) gf :
+ (∀ A, (g A)^f = gf A^f) → (lin_mx g)^f = lin_mx gf.
End MapRingMatrix.
@@ -2320,22 +2330,22 @@ Type Definition*********************************
Section AssocLeft.
-Variables m n p : nat.
-Implicit Type A : 'M[R]_(m, n).
-Implicit Type B : 'M[R]_(n, p).
+Variables m n p : nat.
+Implicit Type A : 'M[R]_(m, n).
+Implicit Type B : 'M[R]_(n, p).
-Lemma trmx_mul A B : (A ×m B)^T = B^T ×m A^T.
+Lemma trmx_mul A B : (A ×m B)^T = B^T ×m A^T.
-Lemma scalemxAr a A B : a *: (A ×m B) = A ×m (a *: B).
+Lemma scalemxAr a A B : a *: (A ×m B) = A ×m (a *: B).
Lemma mulmx_is_scalable A : scalable (@mulmx _ m n p A).
Canonical mulmx_linear A := AddLinear (mulmx_is_scalable A).
-Definition lin_mulmx A : 'M[R]_(n × p, m × p) := lin_mx (mulmx A).
+Definition lin_mulmx A : 'M[R]_(n × p, m × p) := lin_mx (mulmx A).
Lemma lin_mulmx_is_linear : linear lin_mulmx.
@@ -2349,10 +2359,10 @@ Type Definition*********************************
Section LinMulRow.
-Variables m n : nat.
+Variables m n : nat.
-Definition lin_mul_row u : 'M[R]_(m × n, n) := lin1_mx (mulmx u \o vec_mx).
+Definition lin_mul_row u : 'M[R]_(m × n, n) := lin1_mx (mulmx u \o vec_mx).
Lemma lin_mul_row_is_linear : linear lin_mul_row.
@@ -2360,47 +2370,47 @@ Type Definition*********************************
Canonical lin_mul_row_linear := Linear lin_mul_row_is_linear.
-Lemma mul_vec_lin_row A u : mxvec A ×m lin_mul_row u = u ×m A.
+Lemma mul_vec_lin_row A u : mxvec A ×m lin_mul_row u = u ×m A.
End LinMulRow.
-Lemma mxvec_dotmul m n (A : 'M[R]_(m, n)) u v :
- mxvec (u^T ×m v) ×m (mxvec A)^T = u ×m A ×m v^T.
+Lemma mxvec_dotmul m n (A : 'M[R]_(m, n)) u v :
+ mxvec (u^T ×m v) ×m (mxvec A)^T = u ×m A ×m v^T.
Section MatrixAlgType.
-Variable n' : nat.
+Variable n' : nat.
Canonical matrix_algType :=
- Eval hnf in AlgType R 'M[R]_n (fun k ⇒ scalemxAr k).
+ Eval hnf in AlgType R 'M[R]_n (fun k ⇒ scalemxAr k).
End MatrixAlgType.
-Lemma diag_mxC n (d e : 'rV[R]_n) :
- diag_mx d ×m diag_mx e = diag_mx e ×m diag_mx d.
+Lemma diag_mxC n (d e : 'rV[R]_n) :
+ diag_mx d ×m diag_mx e = diag_mx e ×m diag_mx d.
-Lemma diag_mx_comm n' (d e : 'rV[R]_n'.+1) : GRing.comm (diag_mx d) (diag_mx e).
+Lemma diag_mx_comm n' (d e : 'rV[R]_n'.+1) : GRing.comm (diag_mx d) (diag_mx e).
-Lemma scalar_mxC m n a (A : 'M[R]_(m, n)) : A ×m a%:M = a%:M ×m A.
+Lemma scalar_mxC m n a (A : 'M[R]_(m, n)) : A ×m a%:M = a%:M ×m A.
-Lemma scalar_mx_comm n' a (A : 'M[R]_n'.+1) : GRing.comm A a%:M.
+Lemma scalar_mx_comm n' a (A : 'M[R]_n'.+1) : GRing.comm A a%:M.
-Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A ×m a%:M = a *: A.
+Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A ×m a%:M = a *: A.
-Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B :
- \tr (A ×m B) = \tr (B ×m A).
+Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B :
+ \tr (A ×m B) = \tr (B ×m A).
@@ -2411,48 +2421,48 @@ Type Definition*********************************
@@ -2461,30 +2471,30 @@ Type Definition*********************************
Laplace expansion lemma
@@ -2493,7 +2503,7 @@ Type Definition*********************************
Cramer Rule : adjugate on the left
@@ -2502,10 +2512,10 @@ Type Definition*********************************
Cramer rule : adjugate on the right
@@ -2514,7 +2524,7 @@ Type Definition*********************************
Left inverses are right inverses.
@@ -2523,15 +2533,15 @@ Type Definition*********************************
Only tall matrices have inverses.
@@ -2560,91 +2570,91 @@ Type Definition*********************************
Section Defs.
-Variable n : nat.
-Implicit Type A : 'M[R]_n.
+Variable n : nat.
+Implicit Type A : 'M[R]_n.
-Definition unitmx : pred 'M[R]_n := fun A ⇒ \det A \is a GRing.unit.
-Definition invmx A := if A \in unitmx then (\det A)^-1 *: \adj A else A.
+Definition unitmx : pred 'M[R]_n := fun A ⇒ \det A \is a GRing.unit.
+Definition invmx A := if A \in unitmx then (\det A)^-1 *: \adj A else A.
-Lemma unitmxE A : (A \in unitmx) = (\det A \is a GRing.unit).
+Lemma unitmxE A : (A \in unitmx) = (\det A \is a GRing.unit).
-Lemma unitmx1 : 1%:M \in unitmx.
+Lemma unitmx1 : 1%:M \in unitmx.
-Lemma unitmx_perm s : perm_mx s \in unitmx.
+Lemma unitmx_perm s : perm_mx s \in unitmx.
-Lemma unitmx_tr A : (A^T \in unitmx) = (A \in unitmx).
+Lemma unitmx_tr A : (A^T \in unitmx) = (A \in unitmx).
-Lemma unitmxZ a A : a \is a GRing.unit → (a *: A \in unitmx) = (A \in unitmx).
+Lemma unitmxZ a A : a \is a GRing.unit → (a *: A \in unitmx) = (A \in unitmx).
-Lemma invmx1 : invmx 1%:M = 1%:M.
+Lemma invmx1 : invmx 1%:M = 1%:M.
-Lemma invmxZ a A : a *: A \in unitmx → invmx (a *: A) = a^-1 *: invmx A.
+Lemma invmxZ a A : a *: A \in unitmx → invmx (a *: A) = a^-1 *: invmx A.
-Lemma invmx_scalar a : invmx (a%:M) = a^-1%:M.
+Lemma invmx_scalar a : invmx (a%:M) = a^-1%:M.
-Lemma mulVmx : {in unitmx, left_inverse 1%:M invmx mulmx}.
+Lemma mulVmx : {in unitmx, left_inverse 1%:M invmx mulmx}.
-Lemma mulmxV : {in unitmx, right_inverse 1%:M invmx mulmx}.
+Lemma mulmxV : {in unitmx, right_inverse 1%:M invmx mulmx}.
-Lemma mulKmx m : {in unitmx, @left_loop _ 'M_(n, m) invmx mulmx}.
+Lemma mulKmx m : {in unitmx, @left_loop _ 'M_(n, m) invmx mulmx}.
-Lemma mulKVmx m : {in unitmx, @rev_left_loop _ 'M_(n, m) invmx mulmx}.
+Lemma mulKVmx m : {in unitmx, @rev_left_loop _ 'M_(n, m) invmx mulmx}.
-Lemma mulmxK m : {in unitmx, @right_loop 'M_(m, n) _ invmx mulmx}.
+Lemma mulmxK m : {in unitmx, @right_loop 'M_(m, n) _ invmx mulmx}.
-Lemma mulmxKV m : {in unitmx, @rev_right_loop 'M_(m, n) _ invmx mulmx}.
+Lemma mulmxKV m : {in unitmx, @rev_right_loop 'M_(m, n) _ invmx mulmx}.
-Lemma det_inv A : \det (invmx A) = (\det A)^-1.
+Lemma det_inv A : \det (invmx A) = (\det A)^-1.
-Lemma unitmx_inv A : (invmx A \in unitmx) = (A \in unitmx).
+Lemma unitmx_inv A : (invmx A \in unitmx) = (A \in unitmx).
-Lemma unitmx_mul A B : (A ×m B \in unitmx) = (A \in unitmx) && (B \in unitmx).
+Lemma unitmx_mul A B : (A ×m B \in unitmx) = (A \in unitmx) && (B \in unitmx).
-Lemma trmx_inv (A : 'M_n) : (invmx A)^T = invmx (A^T).
+Lemma trmx_inv (A : 'M_n) : (invmx A)^T = invmx (A^T).
-Lemma invmxK : involutive invmx.
+Lemma invmxK : involutive invmx.
-Lemma mulmx1_unit A B : A ×m B = 1%:M → A \in unitmx ∧ B \in unitmx.
+Lemma mulmx1_unit A B : A ×m B = 1%:M → A \in unitmx ∧ B \in unitmx.
-Lemma intro_unitmx A B : B ×m A = 1%:M ∧ A ×m B = 1%:M → unitmx A.
+Lemma intro_unitmx A B : B ×m A = 1%:M ∧ A ×m B = 1%:M → unitmx A.
-Lemma invmx_out : {in [predC unitmx], invmx =1 id}.
+Lemma invmx_out : {in [predC unitmx], invmx =1 id}.
End Defs.
-Variable n' : nat.
+Variable n' : nat.
Definition matrix_unitRingMixin :=
UnitRingMixin (@mulVmx n) (@mulmxV n) (@intro_unitmx n) (@invmx_out n).
Canonical matrix_unitRing :=
- Eval hnf in UnitRingType 'M[R]_n matrix_unitRingMixin.
-Canonical matrix_unitAlg := Eval hnf in [unitAlgType R of 'M[R]_n].
+ Eval hnf in UnitRingType 'M[R]_n matrix_unitRingMixin.
+Canonical matrix_unitAlg := Eval hnf in [unitAlgType R of 'M[R]_n].
@@ -2655,25 +2665,29 @@ Type Definition*********************************
@@ -2684,17 +2698,17 @@ Type Definition*********************************
Section FinUnitMatrix.
-Variables (n : nat) (R : finComUnitRingType).
+Variables (n : nat) (R : finComUnitRingType).
Canonical matrix_finUnitRingType n' :=
- Eval hnf in [finUnitRingType of 'M[R]_n'.+1].
+ Eval hnf in [finUnitRingType of 'M[R]_n'.+1].
-Definition GLtype of phant R := {unit 'M[R]_n.-1.+1}.
+Definition GLtype of phant R := {unit 'M[R]_n.-1.+1}.
-Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 :=
+Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 :=
let: FinRing.Unit A _ := u in A.
@@ -2703,9 +2717,9 @@ Type Definition*********************************
-Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R))
+Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R))
(at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope.
-Notation "{ ''GL_' n ( p ) }" := {'GL_n['F_p]}
+Notation "{ ''GL_' n ( p ) }" := {'GL_n['F_p]}
(at level 0, n at level 2, p at level 10,
format "{ ''GL_' n ( p ) }") : type_scope.
@@ -2713,48 +2727,48 @@ Type Definition*********************************
Section GL_unit.
-Variables (n : nat) (R : finComUnitRingType).
+Variables (n : nat) (R : finComUnitRingType).
-Canonical GL_subType := [subType of {'GL_n[R]} for GLval].
-Definition GL_eqMixin := Eval hnf in [eqMixin of {'GL_n[R]} by <:].
-Canonical GL_eqType := Eval hnf in EqType {'GL_n[R]} GL_eqMixin.
-Canonical GL_choiceType := Eval hnf in [choiceType of {'GL_n[R]}].
-Canonical GL_countType := Eval hnf in [countType of {'GL_n[R]}].
-Canonical GL_subCountType := Eval hnf in [subCountType of {'GL_n[R]}].
-Canonical GL_finType := Eval hnf in [finType of {'GL_n[R]}].
-Canonical GL_subFinType := Eval hnf in [subFinType of {'GL_n[R]}].
-Canonical GL_baseFinGroupType := Eval hnf in [baseFinGroupType of {'GL_n[R]}].
-Canonical GL_finGroupType := Eval hnf in [finGroupType of {'GL_n[R]}].
-Definition GLgroup of phant R := [set: {'GL_n[R]}].
-Canonical GLgroup_group ph := Eval hnf in [group of GLgroup ph].
+Canonical GL_subType := [subType of {'GL_n[R]} for GLval].
+Definition GL_eqMixin := Eval hnf in [eqMixin of {'GL_n[R]} by <:].
+Canonical GL_eqType := Eval hnf in EqType {'GL_n[R]} GL_eqMixin.
+Canonical GL_choiceType := Eval hnf in [choiceType of {'GL_n[R]}].
+Canonical GL_countType := Eval hnf in [countType of {'GL_n[R]}].
+Canonical GL_subCountType := Eval hnf in [subCountType of {'GL_n[R]}].
+Canonical GL_finType := Eval hnf in [finType of {'GL_n[R]}].
+Canonical GL_subFinType := Eval hnf in [subFinType of {'GL_n[R]}].
+Canonical GL_baseFinGroupType := Eval hnf in [baseFinGroupType of {'GL_n[R]}].
+Canonical GL_finGroupType := Eval hnf in [finGroupType of {'GL_n[R]}].
+Definition GLgroup of phant R := [set: {'GL_n[R]}].
+Canonical GLgroup_group ph := Eval hnf in [group of GLgroup ph].
-Implicit Types u v : {'GL_n[R]}.
+Implicit Types u v : {'GL_n[R]}.
-Lemma GL_1E : GLval 1 = 1.
-Lemma GL_VE u : GLval u^-1 = (GLval u)^-1.
-Lemma GL_VxE u : GLval u^-1 = invmx u.
-Lemma GL_ME u v : GLval (u × v) = GLval u × GLval v.
-Lemma GL_MxE u v : GLval (u × v) = u ×m v.
-Lemma GL_unit u : GLval u \is a GRing.unit.
-Lemma GL_unitmx u : val u \in unitmx.
+Lemma GL_1E : GLval 1 = 1.
+Lemma GL_VE u : GLval u^-1 = (GLval u)^-1.
+Lemma GL_VxE u : GLval u^-1 = invmx u.
+Lemma GL_ME u v : GLval (u × v) = GLval u × GLval v.
+Lemma GL_MxE u v : GLval (u × v) = u ×m v.
+Lemma GL_unit u : GLval u \is a GRing.unit.
+Lemma GL_unitmx u : val u \in unitmx.
-Lemma GL_det u : \det u != 0.
+Lemma GL_det u : \det u != 0.
End GL_unit.
-Notation "''GL_' n [ R ]" := (GLgroup n (Phant R))
+Notation "''GL_' n [ R ]" := (GLgroup n (Phant R))
(at level 8, n at level 2, format "''GL_' n [ R ]") : group_scope.
-Notation "''GL_' n ( p )" := 'GL_n['F_p]
+Notation "''GL_' n ( p )" := 'GL_n['F_p]
(at level 8, n at level 2, p at level 10,
format "''GL_' n ( p )") : group_scope.
-Notation "''GL_' n [ R ]" := (GLgroup_group n (Phant R)) : Group_scope.
-Notation "''GL_' n ( p )" := (GLgroup_group n (Phant 'F_p)) : Group_scope.
+Notation "''GL_' n [ R ]" := (GLgroup_group n (Phant R)) : Group_scope.
+Notation "''GL_' n ( p )" := (GLgroup_group n (Phant 'F_p)) : Group_scope.
@@ -2771,16 +2785,16 @@ Type Definition*********************************
Variable R : idomainType.
-Lemma scalemx_eq0 m n a (A : 'M[R]_(m, n)) :
- (a *: A == 0) = (a == 0) || (A == 0).
+Lemma scalemx_eq0 m n a (A : 'M[R]_(m, n)) :
+ (a *: A == 0) = (a == 0) || (A == 0).
Lemma scalemx_inj m n a :
- a != 0 → injective ( *:%R a : 'M[R]_(m, n) → 'M[R]_(m, n)).
+ a != 0 → injective ( *:%R a : 'M[R]_(m, n) → 'M[R]_(m, n)).
-Lemma det0P n (A : 'M[R]_n) :
- reflect (exists2 v : 'rV[R]_n, v != 0 & v ×m A = 0) (\det A == 0).
+Lemma det0P n (A : 'M[R]_n) :
+ reflect (exists2 v : 'rV[R]_n, v != 0 & v ×m A = 0) (\det A == 0).
End MatrixDomain.
@@ -2798,33 +2812,35 @@ Type Definition*********************************
Section MapFieldMatrix.
-Variables (aF : fieldType) (rF : comUnitRingType) (f : {rmorphism aF → rF}).
+Variables (aF : fieldType) (rF : comUnitRingType) (f : {rmorphism aF → rF}).
-Lemma map_mx_inj m n : injective ((map_mx f) m n).
+Lemma map_mx_inj {m n} : injective (map_mx f : 'M_(m, n) → 'M_(m, n)).
-Lemma map_mx_is_scalar n (A : 'M_n) : is_scalar_mx A^f = is_scalar_mx A.
+Lemma map_mx_is_scalar n (A : 'M_n) : is_scalar_mx A^f = is_scalar_mx A.
-Lemma map_unitmx n (A : 'M_n) : (A^f \in unitmx) = (A \in unitmx).
+Lemma map_unitmx n (A : 'M_n) : (A^f \in unitmx) = (A \in unitmx).
-Lemma map_mx_unit n' (A : 'M_n'.+1) :
- (A^f \is a GRing.unit) = (A \is a GRing.unit).
+Lemma map_mx_unit n' (A : 'M_n'.+1) :
+ (A^f \is a GRing.unit) = (A \is a GRing.unit).
-Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f.
+Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f.
-Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1.
+Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1.
-Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0).
+Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0).
End MapFieldMatrix.
+
+
@@ -2860,37 +2876,37 @@ Type Definition*********************************
Fixpoint cormen_lup {n} :=
- match n return let M := 'M[F]_n.+1 in M → M × M × M with
- | 0 ⇒ fun A ⇒ (1, 1, A)
- | _.+1 ⇒ fun A ⇒
- let k := odflt 0 [pick k | A k 0 != 0] in
- let A1 : 'M_(1 + _) := xrow 0 k A in
- let P1 : 'M_(1 + _) := tperm_mx 0 k in
- let Schur := ((A k 0)^-1 *: dlsubmx A1) ×m ursubmx A1 in
- let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in
- let P := block_mx 1 0 0 P2 ×m P1 in
- let L := block_mx 1 0 ((A k 0)^-1 *: (P2 ×m dlsubmx A1)) L2 in
+ match n return let M := 'M[F]_n.+1 in M → M × M × M with
+ | 0 ⇒ fun A ⇒ (1, 1, A)
+ | _.+1 ⇒ fun A ⇒
+ let k := odflt 0 [pick k | A k 0 != 0] in
+ let A1 : 'M_(1 + _) := xrow 0 k A in
+ let P1 : 'M_(1 + _) := tperm_mx 0 k in
+ let Schur := ((A k 0)^-1 *: dlsubmx A1) ×m ursubmx A1 in
+ let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in
+ let P := block_mx 1 0 0 P2 ×m P1 in
+ let L := block_mx 1 0 ((A k 0)^-1 *: (P2 ×m dlsubmx A1)) L2 in
let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in
- (P, L, U)
+ (P, L, U)
end.
-Lemma cormen_lup_perm n (A : 'M_n.+1) : is_perm_mx (cormen_lup A).1.1.
+Lemma cormen_lup_perm n (A : 'M_n.+1) : is_perm_mx (cormen_lup A).1.1.
-Lemma cormen_lup_correct n (A : 'M_n.+1) :
- let: (P, L, U) := cormen_lup A in P × A = L × U.
+Lemma cormen_lup_correct n (A : 'M_n.+1) :
+ let: (P, L, U) := cormen_lup A in P × A = L × U.
-Lemma cormen_lup_detL n (A : 'M_n.+1) : \det (cormen_lup A).1.2 = 1.
+Lemma cormen_lup_detL n (A : 'M_n.+1) : \det (cormen_lup A).1.2 = 1.
-Lemma cormen_lup_lower n A (i j : 'I_n.+1) :
- i ≤ j → (cormen_lup A).1.2 i j = (i == j)%:R.
+Lemma cormen_lup_lower n A (i j : 'I_n.+1) :
+ i ≤ j → (cormen_lup A).1.2 i j = (i == j)%:R.
-Lemma cormen_lup_upper n A (i j : 'I_n.+1) :
- j < i → (cormen_lup A).2 i j = 0 :> F.
+Lemma cormen_lup_upper n A (i j : 'I_n.+1) :
+ j < i → (cormen_lup A).2 i j = 0 :> F.
End CormenLUP.
--
cgit v1.2.3