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.mxalgebra.html | 1394 +++++++++++++------------- 1 file changed, 701 insertions(+), 693 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.mxalgebra.html') diff --git a/docs/htmldoc/mathcomp.algebra.mxalgebra.html b/docs/htmldoc/mathcomp.algebra.mxalgebra.html index 5ab8faa..cbd9867 100644 --- a/docs/htmldoc/mathcomp.algebra.mxalgebra.html +++ b/docs/htmldoc/mathcomp.algebra.mxalgebra.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -161,27 +160,27 @@ Reserved Notation "A ^C" (at level 8, format "A ^C").

-Notation "''A_' ( m , n )" := 'M_(m, n ^ 2)
+Notation "''A_' ( m , n )" := 'M_(m, n ^ 2)
  (at level 8, format "''A_' ( m , n )") : type_scope.

-Notation "''A_' ( n )" := 'A_(n ^ 2, n)
+Notation "''A_' ( n )" := 'A_(n ^ 2, n)
  (at level 8, only parsing) : type_scope.

-Notation "''A_' n" := 'A_(n)
+Notation "''A_' n" := 'A_(n)
  (at level 8, n at next level, format "''A_' n") : type_scope.

-Notation "''A' [ F ]_ ( m , n )" := 'M[F]_(m, n ^ 2)
+Notation "''A' [ F ]_ ( m , n )" := 'M[F]_(m, n ^ 2)
  (at level 8, only parsing) : type_scope.

-Notation "''A' [ F ]_ ( n )" := 'A[F]_(n ^ 2, n)
+Notation "''A' [ F ]_ ( n )" := 'A[F]_(n ^ 2, n)
  (at level 8, only parsing) : type_scope.

-Notation "''A' [ F ]_ n" := 'A[F]_(n)
+Notation "''A' [ F ]_ n" := 'A[F]_(n)
  (at level 8, n at level 2, only parsing) : type_scope.

@@ -202,7 +201,7 @@
Variable F : fieldType.
-Implicit Types m n p r : nat.
+Implicit Types m n p r : nat.

@@ -216,51 +215,51 @@

-Fixpoint Gaussian_elimination {m n} : 'M_(m, n) → 'M_m × 'M_n × nat :=
+Fixpoint Gaussian_elimination {m n} : 'M_(m, n) → 'M_m × 'M_n × nat :=
  match m, n with
-  | _.+1, _.+1 ⇒ fun A : 'M_(1 + _, 1 + _) ⇒
-    if [pick ij | A ij.1 ij.2 != 0] is Some (i, j) then
+  | _.+1, _.+1 ⇒ fun A : 'M_(1 + _, 1 + _) ⇒
+    if [pick ij | A ij.1 ij.2 != 0] is Some (i, j) then
      let a := A i j in let A1 := xrow i 0 (xcol j 0 A) in
-      let u := ursubmx A1 in let v := a^-1 *: dlsubmx A1 in
-      let: (L, U, r) := Gaussian_elimination (drsubmx A1 - v ×m u) in
-      (xrow i 0 (block_mx 1 0 v L), xcol j 0 (block_mx a%:M u 0 U), r.+1)
-    else (1%:M, 1%:M, 0%N)
-  | _, _ ⇒ fun _ ⇒ (1%:M, 1%:M, 0%N)
+      let u := ursubmx A1 in let v := a^-1 *: dlsubmx A1 in
+      let: (L, U, r) := Gaussian_elimination (drsubmx A1 - v ×m u) in
+      (xrow i 0 (block_mx 1 0 v L), xcol j 0 (block_mx a%:M u 0 U), r.+1)
+    else (1%:M, 1%:M, 0%N)
+  | _, _ ⇒ fun _ ⇒ (1%:M, 1%:M, 0%N)
  end.

Section Defs.

-Variables (m n : nat) (A : 'M_(m, n)).
+Variables (m n : nat) (A : 'M_(m, n)).

-Fact Gaussian_elimination_key : unit.
+Fact Gaussian_elimination_key : unit.

-Let LUr := locked_with Gaussian_elimination_key (@Gaussian_elimination) m n A.
+Let LUr := locked_with Gaussian_elimination_key (@Gaussian_elimination) m n A.

-Definition col_ebase := LUr.1.1.
-Definition row_ebase := LUr.1.2.
-Definition mxrank := if [|| m == 0 | n == 0]%N then 0%N else LUr.2.
+Definition col_ebase := LUr.1.1.
+Definition row_ebase := LUr.1.2.
+Definition mxrank := if [|| m == 0 | n == 0]%N then 0%N else LUr.2.

-Definition row_free := mxrank == m.
-Definition row_full := mxrank == n.
+Definition row_free := mxrank == m.
+Definition row_full := mxrank == n.

-Definition row_base : 'M_(mxrank, n) := pid_mx mxrank ×m row_ebase.
-Definition col_base : 'M_(m, mxrank) := col_ebase ×m pid_mx mxrank.
+Definition row_base : 'M_(mxrank, n) := pid_mx mxrank ×m row_ebase.
+Definition col_base : 'M_(m, mxrank) := col_ebase ×m pid_mx mxrank.

-Definition complmx : 'M_n := copid_mx mxrank ×m row_ebase.
-Definition kermx : 'M_m := copid_mx mxrank ×m invmx col_ebase.
-Definition cokermx : 'M_n := invmx row_ebase ×m copid_mx mxrank.
+Definition complmx : 'M_n := copid_mx mxrank ×m row_ebase.
+Definition kermx : 'M_m := copid_mx mxrank ×m invmx col_ebase.
+Definition cokermx : 'M_n := invmx row_ebase ×m copid_mx mxrank.

-Definition pinvmx : 'M_(n, m) :=
-  invmx row_ebase ×m pid_mx mxrank ×m invmx col_ebase.
+Definition pinvmx : 'M_(n, m) :=
+  invmx row_ebase ×m pid_mx mxrank ×m invmx col_ebase.

End Defs.
@@ -268,41 +267,41 @@

-Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
-  A ×m cokermx B == 0).
-Fact submx_key : unit.
-Definition submx := locked_with submx_key submx_def.
-Canonical submx_unlockable := [unlockable fun submx].
+Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
+  A ×m cokermx B == 0).
+Fact submx_key : unit.
+Definition submx := locked_with submx_key submx_def.
+Canonical submx_unlockable := [unlockable fun submx].


-Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
-  (A ≤ B)%MS && ~~ (B ≤ A)%MS.
+Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
+  (A ≤ B)%MS && ~~ (B ≤ A)%MS.

-Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
-  prod (\rank A = \rank B)
-       (∀ m3 (C : 'M_(m3, n)),
-            ((A ≤ C) = (B ≤ C)) × ((C ≤ A) = (C ≤ B)))%MS.
+Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
+  prod (\rank A = \rank B)
+       (∀ m3 (C : 'M_(m3, n)),
+            ((A ≤ C) = (B ≤ C)) × ((C ≤ A) = (C ≤ B)))%MS.

Section LtmxIdentities.

-Variables (m1 m2 n : nat) (A : 'M_(m1, n)) (B : 'M_(m2, n)).
+Variables (m1 m2 n : nat) (A : 'M_(m1, n)) (B : 'M_(m2, n)).

-Lemma ltmxE : (A < B)%MS = ((A ≤ B)%MS && ~~ (B ≤ A)%MS).
+Lemma ltmxE : (A < B)%MS = ((A ≤ B)%MS && ~~ (B ≤ A)%MS).

-Lemma ltmxW : (A < B)%MS → (A ≤ B)%MS.
+Lemma ltmxW : (A < B)%MS → (A ≤ B)%MS.

-Lemma ltmxEneq : (A < B)%MS = (A ≤ B)%MS && ~~ (A == B)%MS.
+Lemma ltmxEneq : (A < B)%MS = (A ≤ B)%MS && ~~ (A == B)%MS.

-Lemma submxElt : (A ≤ B)%MS = (A == B)%MS || (A < B)%MS.
+Lemma submxElt : (A ≤ B)%MS = (A == B)%MS || (A < B)%MS.

End LtmxIdentities.
@@ -324,19 +323,19 @@ row_base A padded with null rows.
-Let qidmx m n (A : 'M_(m, n)) :=
-  if m == n then A == pid_mx n else row_full A.
-Let equivmx m n (A : 'M_(m, n)) idA (B : 'M_n) :=
-  (B == A)%MS && (qidmx B == idA).
-Let equivmx_spec m n (A : 'M_(m, n)) idA (B : 'M_n) :=
-  prod (B :=: A)%MS (qidmx B = idA).
-Definition genmx_witness m n (A : 'M_(m, n)) : 'M_n :=
-  if row_full A then 1%:M else pid_mx (\rank A) ×m row_ebase A.
-Definition genmx_def := idfun (fun m n (A : 'M_(m, n)) ⇒
-   choose (equivmx A (row_full A)) (genmx_witness A) : 'M_n).
-Fact genmx_key : unit.
-Definition genmx := locked_with genmx_key genmx_def.
-Canonical genmx_unlockable := [unlockable fun genmx].
+Let qidmx m n (A : 'M_(m, n)) :=
+  if m == n then A == pid_mx n else row_full A.
+Let equivmx m n (A : 'M_(m, n)) idA (B : 'M_n) :=
+  (B == A)%MS && (qidmx B == idA).
+Let equivmx_spec m n (A : 'M_(m, n)) idA (B : 'M_n) :=
+  prod (B :=: A)%MS (qidmx B = idA).
+Definition genmx_witness m n (A : 'M_(m, n)) : 'M_n :=
+  if row_full A then 1%:M else pid_mx (\rank A) ×m row_ebase A.
+Definition genmx_def := idfun (fun m n (A : 'M_(m, n)) ⇒
+   choose (equivmx A (row_full A)) (genmx_witness A) : 'M_n).
+Fact genmx_key : unit.
+Definition genmx := locked_with genmx_key genmx_def.
+Canonical genmx_unlockable := [unlockable fun genmx].

@@ -347,13 +346,13 @@ setwise sum is not quite strictly extensional.
-Let addsmx_nop m n (A : 'M_(m, n)) := conform_mx <<A>>%MS A.
-Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
-  if A == 0 then addsmx_nop B else if B == 0 then addsmx_nop A else
-  <<col_mx A B>>%MS : 'M_n).
-Fact addsmx_key : unit.
-Definition addsmx := locked_with addsmx_key addsmx_def.
-Canonical addsmx_unlockable := [unlockable fun addsmx].
+Let addsmx_nop m n (A : 'M_(m, n)) := conform_mx <<A>>%MS A.
+Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
+  if A == 0 then addsmx_nop B else if B == 0 then addsmx_nop A else
+  <<col_mx A B>>%MS : 'M_n).
+Fact addsmx_key : unit.
+Definition addsmx := locked_with addsmx_key addsmx_def.
+Canonical addsmx_unlockable := [unlockable fun addsmx].

@@ -374,455 +373,455 @@ showing that associativity is strict.
-Let capmx_witness m n (A : 'M_(m, n)) :=
-  if row_full A then conform_mx 1%:M A else <<A>>%MS.
-Let capmx_norm m n (A : 'M_(m, n)) :=
+Let capmx_witness m n (A : 'M_(m, n)) :=
+  if row_full A then conform_mx 1%:M A else <<A>>%MS.
+Let capmx_norm m n (A : 'M_(m, n)) :=
  choose (equivmx A (qidmx A)) (capmx_witness A).
-Let capmx_nop m n (A : 'M_(m, n)) := conform_mx (capmx_norm A) A.
-Definition capmx_gen m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
-  lsubmx (kermx (col_mx A B)) ×m A.
-Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
-  if qidmx A then capmx_nop B else
-  if qidmx B then capmx_nop A else
-  if row_full B then capmx_norm A else capmx_norm (capmx_gen A B) : 'M_n).
-Fact capmx_key : unit.
-Definition capmx := locked_with capmx_key capmx_def.
-Canonical capmx_unlockable := [unlockable fun capmx].
+Let capmx_nop m n (A : 'M_(m, n)) := conform_mx (capmx_norm A) A.
+Definition capmx_gen m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
+  lsubmx (kermx (col_mx A B)) ×m A.
+Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
+  if qidmx A then capmx_nop B else
+  if qidmx B then capmx_nop A else
+  if row_full B then capmx_norm A else capmx_norm (capmx_gen A B) : 'M_n).
+Fact capmx_key : unit.
+Definition capmx := locked_with capmx_key capmx_def.
+Canonical capmx_unlockable := [unlockable fun capmx].

-Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
-  <<capmx_gen A (capmx_gen A B)^C>>%MS : 'M_n).
-Fact diffmx_key : unit.
-Definition diffmx := locked_with diffmx_key diffmx_def.
-Canonical diffmx_unlockable := [unlockable fun diffmx].
+Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) ⇒
+  <<capmx_gen A (capmx_gen A B)^C>>%MS : 'M_n).
+Fact diffmx_key : unit.
+Definition diffmx := locked_with diffmx_key diffmx_def.
+Canonical diffmx_unlockable := [unlockable fun diffmx].

-Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) ×m col_mx U 0.
+Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) ×m col_mx U 0.


-Fact mxrankE m n (A : 'M_(m, n)) : \rank A = (GaussE A).2.
+Fact mxrankE m n (A : 'M_(m, n)) : \rank A = (GaussE A).2.

-Lemma rank_leq_row m n (A : 'M_(m, n)) : \rank A ≤ m.
+Lemma rank_leq_row m n (A : 'M_(m, n)) : \rank A ≤ m.

-Lemma row_leq_rank m n (A : 'M_(m, n)) : (m ≤ \rank A) = row_free A.
+Lemma row_leq_rank m n (A : 'M_(m, n)) : (m ≤ \rank A) = row_free A.

-Lemma rank_leq_col m n (A : 'M_(m, n)) : \rank A ≤ n.
+Lemma rank_leq_col m n (A : 'M_(m, n)) : \rank A ≤ n.

-Lemma col_leq_rank m n (A : 'M_(m, n)) : (n ≤ \rank A) = row_full A.
+Lemma col_leq_rank m n (A : 'M_(m, n)) : (n ≤ \rank A) = row_full A.

Let unitmx1F := @unitmx1 F.
-Lemma row_ebase_unit m n (A : 'M_(m, n)) : row_ebase A \in unitmx.
+Lemma row_ebase_unit m n (A : 'M_(m, n)) : row_ebase A \in unitmx.

-Lemma col_ebase_unit m n (A : 'M_(m, n)) : col_ebase A \in unitmx.
-Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit.
+Lemma col_ebase_unit m n (A : 'M_(m, n)) : col_ebase A \in unitmx.
+Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit : core.

-Lemma mulmx_ebase m n (A : 'M_(m, n)) :
-  col_ebase A ×m pid_mx (\rank A) ×m row_ebase A = A.
+Lemma mulmx_ebase m n (A : 'M_(m, n)) :
+  col_ebase A ×m pid_mx (\rank A) ×m row_ebase A = A.

-Lemma mulmx_base m n (A : 'M_(m, n)) : col_base A ×m row_base A = A.
+Lemma mulmx_base m n (A : 'M_(m, n)) : col_base A ×m row_base A = A.

-Lemma mulmx1_min_rank r m n (A : 'M_(m, n)) M N :
-  M ×m A ×m N = 1%:M :> 'M_r → r ≤ \rank A.
+Lemma mulmx1_min_rank r m n (A : 'M_(m, n)) M N :
+  M ×m A ×m N = 1%:M :> 'M_r → r ≤ \rank A.

-Lemma mulmx_max_rank r m n (M : 'M_(m, r)) (N : 'M_(r, n)) :
-  \rank (M ×m N) ≤ r.
+Lemma mulmx_max_rank r m n (M : 'M_(m, r)) (N : 'M_(r, n)) :
+  \rank (M ×m N) ≤ r.

-Lemma mxrank_tr m n (A : 'M_(m, n)) : \rank A^T = \rank A.
+Lemma mxrank_tr m n (A : 'M_(m, n)) : \rank A^T = \rank A.

-Lemma mxrank_add m n (A B : 'M_(m, n)) : \rank (A + B)%R ≤ \rank A + \rank B.
+Lemma mxrank_add m n (A B : 'M_(m, n)) : \rank (A + B)%R ≤ \rank A + \rank B.

-Lemma mxrankM_maxl m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  \rank (A ×m B) ≤ \rank A.
+Lemma mxrankM_maxl m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  \rank (A ×m B) ≤ \rank A.

-Lemma mxrankM_maxr m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  \rank (A ×m B) ≤ \rank B.
+Lemma mxrankM_maxr m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  \rank (A ×m B) ≤ \rank B.

-Lemma mxrank_scale m n a (A : 'M_(m, n)) : \rank (a *: A) ≤ \rank A.
+Lemma mxrank_scale m n a (A : 'M_(m, n)) : \rank (a *: A) ≤ \rank A.

-Lemma mxrank_scale_nz m n a (A : 'M_(m, n)) :
-   a != 0 → \rank (a *: A) = \rank A.
+Lemma mxrank_scale_nz m n a (A : 'M_(m, n)) :
+   a != 0 → \rank (a *: A) = \rank A.

-Lemma mxrank_opp m n (A : 'M_(m, n)) : \rank (- A) = \rank A.
+Lemma mxrank_opp m n (A : 'M_(m, n)) : \rank (- A) = \rank A.

-Lemma mxrank0 m n : \rank (0 : 'M_(m, n)) = 0%N.
+Lemma mxrank0 m n : \rank (0 : 'M_(m, n)) = 0%N.

-Lemma mxrank_eq0 m n (A : 'M_(m, n)) : (\rank A == 0%N) = (A == 0).
+Lemma mxrank_eq0 m n (A : 'M_(m, n)) : (\rank A == 0%N) = (A == 0).

-Lemma mulmx_coker m n (A : 'M_(m, n)) : A ×m cokermx A = 0.
+Lemma mulmx_coker m n (A : 'M_(m, n)) : A ×m cokermx A = 0.

-Lemma submxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS = (A ×m cokermx B == 0).
+Lemma submxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS = (A ×m cokermx B == 0).

-Lemma mulmxKpV m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS → A ×m pinvmx B ×m B = A.
+Lemma mulmxKpV m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS → A ×m pinvmx B ×m B = A.

-Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (∃ D, A = D ×m B) (A ≤ B)%MS.
+Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (∃ D, A = D ×m B) (A ≤ B)%MS.

-Lemma submx_refl m n (A : 'M_(m, n)) : (A ≤ A)%MS.
- Hint Resolve submx_refl.
+Lemma submx_refl m n (A : 'M_(m, n)) : (A ≤ A)%MS.
+ Hint Resolve submx_refl : core.

-Lemma submxMl m n p (D : 'M_(m, n)) (A : 'M_(n, p)) : (D ×m A ≤ A)%MS.
+Lemma submxMl m n p (D : 'M_(m, n)) (A : 'M_(n, p)) : (D ×m A ≤ A)%MS.

-Lemma submxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  (A ≤ B)%MS → (A ×m C ≤ B ×m C)%MS.
+Lemma submxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  (A ≤ B)%MS → (A ×m C ≤ B ×m C)%MS.

-Lemma mulmx_sub m n1 n2 p (C : 'M_(m, n1)) A (B : 'M_(n2, p)) :
-  (A ≤ B → C ×m A ≤ B)%MS.
+Lemma mulmx_sub m n1 n2 p (C : 'M_(m, n1)) A (B : 'M_(n2, p)) :
+  (A ≤ B → C ×m A ≤ B)%MS.

Lemma submx_trans m1 m2 m3 n
-                 (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A ≤ B → B ≤ C → A ≤ C)%MS.
+                 (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A ≤ B → B ≤ C → A ≤ C)%MS.

Lemma ltmx_sub_trans m1 m2 m3 n
-                     (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A < B)%MS → (B ≤ C)%MS → (A < C)%MS.
+                     (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A < B)%MS → (B ≤ C)%MS → (A < C)%MS.

Lemma sub_ltmx_trans m1 m2 m3 n
-                     (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A ≤ B)%MS → (B < C)%MS → (A < C)%MS.
+                     (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A ≤ B)%MS → (B < C)%MS → (A < C)%MS.

-Lemma ltmx_trans m n : transitive (@ltmx m m n).
+Lemma ltmx_trans m n : transitive (@ltmx m m n).

-Lemma ltmx_irrefl m n : irreflexive (@ltmx m m n).
+Lemma ltmx_irrefl m n : irreflexive (@ltmx m m n).

-Lemma sub0mx m1 m2 n (A : 'M_(m2, n)) : ((0 : 'M_(m1, n)) ≤ A)%MS.
+Lemma sub0mx m1 m2 n (A : 'M_(m2, n)) : ((0 : 'M_(m1, n)) ≤ A)%MS.

-Lemma submx0null m1 m2 n (A : 'M[F]_(m1, n)) :
-  (A ≤ (0 : 'M_(m2, n)))%MS → A = 0.
+Lemma submx0null m1 m2 n (A : 'M[F]_(m1, n)) :
+  (A ≤ (0 : 'M_(m2, n)))%MS → A = 0.

-Lemma submx0 m n (A : 'M_(m, n)) : (A ≤ (0 : 'M_n))%MS = (A == 0).
+Lemma submx0 m n (A : 'M_(m, n)) : (A ≤ (0 : 'M_n))%MS = (A == 0).

-Lemma lt0mx m n (A : 'M_(m, n)) : ((0 : 'M_n) < A)%MS = (A != 0).
+Lemma lt0mx m n (A : 'M_(m, n)) : ((0 : 'M_n) < A)%MS = (A != 0).

-Lemma ltmx0 m n (A : 'M[F]_(m, n)) : (A < (0 : 'M_n))%MS = false.
+Lemma ltmx0 m n (A : 'M[F]_(m, n)) : (A < (0 : 'M_n))%MS = false.

-Lemma eqmx0P m n (A : 'M_(m, n)) : reflect (A = 0) (A == (0 : 'M_n))%MS.
+Lemma eqmx0P m n (A : 'M_(m, n)) : reflect (A = 0) (A == (0 : 'M_n))%MS.

-Lemma eqmx_eq0 m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :=: B)%MS → (A == 0) = (B == 0).
+Lemma eqmx_eq0 m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :=: B)%MS → (A == 0) = (B == 0).

-Lemma addmx_sub m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m1, n)) (C : 'M_(m2, n)) :
-  (A ≤ C)%MS → (B ≤ C)%MS → ((A + B)%R ≤ C)%MS.
+Lemma addmx_sub m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m1, n)) (C : 'M_(m2, n)) :
+  (A ≤ C)%MS → (B ≤ C)%MS → ((A + B)%R ≤ C)%MS.

-Lemma summx_sub m1 m2 n (B : 'M_(m2, n))
-                I (r : seq I) (P : pred I) (A_ : I → 'M_(m1, n)) :
-  (∀ i, P i → A_ i ≤ B)%MS → ((\sum_(i <- r | P i) A_ i)%R ≤ B)%MS.
+Lemma summx_sub m1 m2 n (B : 'M_(m2, n))
+                I (r : seq I) (P : pred I) (A_ : I → 'M_(m1, n)) :
+  (∀ i, P i → A_ i ≤ B)%MS → ((\sum_(i <- r | P i) A_ i)%R ≤ B)%MS.

-Lemma scalemx_sub m1 m2 n a (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS → (a *: A ≤ B)%MS.
+Lemma scalemx_sub m1 m2 n a (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS → (a *: A ≤ B)%MS.

-Lemma row_sub m n i (A : 'M_(m, n)) : (row i A ≤ A)%MS.
+Lemma row_sub m n i (A : 'M_(m, n)) : (row i A ≤ A)%MS.

-Lemma eq_row_sub m n v (A : 'M_(m, n)) i : row i A = v → (v ≤ A)%MS.
+Lemma eq_row_sub m n v (A : 'M_(m, n)) i : row i A = v → (v ≤ A)%MS.

-Lemma nz_row_sub m n (A : 'M_(m, n)) : (nz_row A ≤ A)%MS.
+Lemma nz_row_sub m n (A : 'M_(m, n)) : (nz_row A ≤ A)%MS.

-Lemma row_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (∀ i, row i A ≤ B)%MS (A ≤ B)%MS.
+Lemma row_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (∀ i, row i A ≤ B)%MS (A ≤ B)%MS.

-Lemma rV_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (∀ v : 'rV_n, v ≤ A → v ≤ B)%MS (A ≤ B)%MS.
+Lemma rV_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (∀ v : 'rV_n, v ≤ A → v ≤ B)%MS (A ≤ B)%MS.

-Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (∃ i, ~~ (row i A ≤ B)%MS) (~~ (A ≤ B)%MS).
+Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (∃ i, ~~ (row i A ≤ B)%MS) (~~ (A ≤ B)%MS).

-Lemma sub_rVP n (u v : 'rV_n) : reflect (∃ a, u = a *: v) (u ≤ v)%MS.
+Lemma sub_rVP n (u v : 'rV_n) : reflect (∃ a, u = a *: v) (u ≤ v)%MS.

-Lemma rank_rV n (v : 'rV_n) : \rank v = (v != 0).
+Lemma rank_rV n (v : 'rV_n) : \rank v = (v != 0).

-Lemma rowV0Pn m n (A : 'M_(m, n)) :
-  reflect (exists2 v : 'rV_n, v ≤ A & v != 0)%MS (A != 0).
+Lemma rowV0Pn m n (A : 'M_(m, n)) :
+  reflect (exists2 v : 'rV_n, v ≤ A & v != 0)%MS (A != 0).

-Lemma rowV0P m n (A : 'M_(m, n)) :
-  reflect (∀ v : 'rV_n, v ≤ A → v = 0)%MS (A == 0).
+Lemma rowV0P m n (A : 'M_(m, n)) :
+  reflect (∀ v : 'rV_n, v ≤ A → v = 0)%MS (A == 0).

-Lemma submx_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  row_full B → (A ≤ B)%MS.
+Lemma submx_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  row_full B → (A ≤ B)%MS.

-Lemma row_fullP m n (A : 'M_(m, n)) :
-  reflect (∃ B, B ×m A = 1%:M) (row_full A).
+Lemma row_fullP m n (A : 'M_(m, n)) :
+  reflect (∃ B, B ×m A = 1%:M) (row_full A).

-Lemma row_full_inj m n p A : row_full A → injective (@mulmx _ m n p A).
+Lemma row_full_inj m n p A : row_full A → injective (@mulmx _ m n p A).

-Lemma row_freeP m n (A : 'M_(m, n)) :
-  reflect (∃ B, A ×m B = 1%:M) (row_free A).
+Lemma row_freeP m n (A : 'M_(m, n)) :
+  reflect (∃ B, A ×m B = 1%:M) (row_free A).

-Lemma row_free_inj m n p A : row_free A → injective ((@mulmx _ m n p)^~ A).
+Lemma row_free_inj m n p A : row_free A → injective ((@mulmx _ m n p)^~ A).

-Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx).
+Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx).

-Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx).
+Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx).

-Lemma mxrank_unit n (A : 'M_n) : A \in unitmx → \rank A = n.
+Lemma mxrank_unit n (A : 'M_n) : A \in unitmx → \rank A = n.

-Lemma mxrank1 n : \rank (1%:M : 'M_n) = n.
+Lemma mxrank1 n : \rank (1%:M : 'M_n) = n.

-Lemma mxrank_delta m n i j : \rank (delta_mx i j : 'M_(m, n)) = 1%N.
+Lemma mxrank_delta m n i j : \rank (delta_mx i j : 'M_(m, n)) = 1%N.

-Lemma mxrankS m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS → \rank A ≤ \rank B.
+Lemma mxrankS m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS → \rank A ≤ \rank B.

-Lemma submx1 m n (A : 'M_(m, n)) : (A ≤ 1%:M)%MS.
+Lemma submx1 m n (A : 'M_(m, n)) : (A ≤ 1%:M)%MS.

-Lemma sub1mx m n (A : 'M_(m, n)) : (1%:M ≤ A)%MS = row_full A.
+Lemma sub1mx m n (A : 'M_(m, n)) : (1%:M ≤ A)%MS = row_full A.

-Lemma ltmx1 m n (A : 'M_(m, n)) : (A < 1%:M)%MS = ~~ row_full A.
+Lemma ltmx1 m n (A : 'M_(m, n)) : (A < 1%:M)%MS = ~~ row_full A.

-Lemma lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false.
+Lemma lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false.

-Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (A :=: B)%MS (A == B)%MS.
+Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (A :=: B)%MS (A == B)%MS.

-Lemma rV_eqP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (∀ u : 'rV_n, (u ≤ A) = (u ≤ B))%MS (A == B)%MS.
+Lemma rV_eqP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (∀ u : 'rV_n, (u ≤ A) = (u ≤ B))%MS (A == B)%MS.

-Lemma eqmx_refl m1 n (A : 'M_(m1, n)) : (A :=: A)%MS.
+Lemma eqmx_refl m1 n (A : 'M_(m1, n)) : (A :=: A)%MS.

-Lemma eqmx_sym m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :=: B)%MS → (B :=: A)%MS.
+Lemma eqmx_sym m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :=: B)%MS → (B :=: A)%MS.

-Lemma eqmx_trans m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A :=: B)%MS → (B :=: C)%MS → (A :=: C)%MS.
+Lemma eqmx_trans m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A :=: B)%MS → (B :=: C)%MS → (A :=: C)%MS.

-Lemma eqmx_rank m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A == B)%MS → \rank A = \rank B.
+Lemma eqmx_rank m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A == B)%MS → \rank A = \rank B.

-Lemma lt_eqmx m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-    (A :=: B)%MS →
-  ∀ C : 'M_(m3, n), (((A < C) = (B < C))%MS × ((C < A) = (C < B))%MS)%type.
+Lemma lt_eqmx m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+    (A :=: B)%MS →
+  ∀ C : 'M_(m3, n), (((A < C) = (B < C))%MS × ((C < A) = (C < B))%MS)%type.

-Lemma eqmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  (A :=: B)%MS → (A ×m C :=: B ×m C)%MS.
+Lemma eqmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  (A :=: B)%MS → (A ×m C :=: B ×m C)%MS.

-Lemma eqmxMfull m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  row_full A → (A ×m B :=: B)%MS.
+Lemma eqmxMfull m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  row_full A → (A ×m B :=: B)%MS.

-Lemma eqmx0 m n : ((0 : 'M[F]_(m, n)) :=: (0 : 'M_n))%MS.
+Lemma eqmx0 m n : ((0 : 'M[F]_(m, n)) :=: (0 : 'M_n))%MS.

-Lemma eqmx_scale m n a (A : 'M_(m, n)) : a != 0 → (a *: A :=: A)%MS.
+Lemma eqmx_scale m n a (A : 'M_(m, n)) : a != 0 → (a *: A :=: A)%MS.

-Lemma eqmx_opp m n (A : 'M_(m, n)) : (- A :=: A)%MS.
+Lemma eqmx_opp m n (A : 'M_(m, n)) : (- A :=: A)%MS.

-Lemma submxMfree m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  row_free C → (A ×m C ≤ B ×m C)%MS = (A ≤ B)%MS.
+Lemma submxMfree m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  row_free C → (A ×m C ≤ B ×m C)%MS = (A ≤ B)%MS.

-Lemma eqmxMfree m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  row_free C → (A ×m C :=: B ×m C)%MS → (A :=: B)%MS.
+Lemma eqmxMfree m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  row_free C → (A ×m C :=: B ×m C)%MS → (A :=: B)%MS.

-Lemma mxrankMfree m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  row_free B → \rank (A ×m B) = \rank A.
+Lemma mxrankMfree m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  row_free B → \rank (A ×m B) = \rank A.

-Lemma eq_row_base m n (A : 'M_(m, n)) : (row_base A :=: A)%MS.
+Lemma eq_row_base m n (A : 'M_(m, n)) : (row_base A :=: A)%MS.

-Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M).
+Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M).

-Let genmx_witnessP m n (A : 'M_(m, n)) :
+Let genmx_witnessP m n (A : 'M_(m, n)) :
  equivmx A (row_full A) (genmx_witness A).

-Lemma genmxE m n (A : 'M_(m, n)) : (<<A>> :=: A)%MS.
+Lemma genmxE m n (A : 'M_(m, n)) : (<<A>> :=: A)%MS.

-Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :=: B → <<A>> = <<B>>)%MS.
+Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :=: B → <<A>> = <<B>>)%MS.

-Lemma genmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (<<A>> = <<B>>)%MS (A == B)%MS.
+Lemma genmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (<<A>> = <<B>>)%MS (A == B)%MS.

-Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.
+Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.

-Lemma genmx1 n : <<1%:M : 'M_n>>%MS = 1%:M.
+Lemma genmx1 n : <<1%:M : 'M_n>>%MS = 1%:M.

-Lemma genmx_id m n (A : 'M_(m, n)) : (<<<<A>>>> = <<A>>)%MS.
+Lemma genmx_id m n (A : 'M_(m, n)) : (<<<<A>>>> = <<A>>)%MS.

-Lemma row_base_free m n (A : 'M_(m, n)) : row_free (row_base A).
+Lemma row_base_free m n (A : 'M_(m, n)) : row_free (row_base A).

-Lemma mxrank_gen m n (A : 'M_(m, n)) : \rank <<A>> = \rank A.
+Lemma mxrank_gen m n (A : 'M_(m, n)) : \rank <<A>> = \rank A.

-Lemma col_base_full m n (A : 'M_(m, n)) : row_full (col_base A).
-Hint Resolve row_base_free col_base_full.
+Lemma col_base_full m n (A : 'M_(m, n)) : row_full (col_base A).
+Hint Resolve row_base_free col_base_full : core.

-Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (B ≤ A)%MS.
+Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (B ≤ A)%MS.

-Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (A == B)%MS.
+Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (A == B)%MS.

-Lemma ltmxErank m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A < B)%MS = (A ≤ B)%MS && (\rank A < \rank B).
+Lemma ltmxErank m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A < B)%MS = (A ≤ B)%MS && (\rank A < \rank B).

-Lemma rank_ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A < B)%MS → \rank A < \rank B.
+Lemma rank_ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A < B)%MS → \rank A < \rank B.

-Lemma eqmx_cast m1 m2 n (A : 'M_(m1, n)) e :
-  ((castmx e A : 'M_(m2, n)) :=: A)%MS.
+Lemma eqmx_cast m1 m2 n (A : 'M_(m1, n)) e :
+  ((castmx e A : 'M_(m2, n)) :=: A)%MS.

-Lemma eqmx_conform m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (conform_mx A B :=: A ∨ conform_mx A B :=: B)%MS.
+Lemma eqmx_conform m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (conform_mx A B :=: A ∨ conform_mx A B :=: B)%MS.

-Let eqmx_sum_nop m n (A : 'M_(m, n)) : (addsmx_nop A :=: A)%MS.
+Let eqmx_sum_nop m n (A : 'M_(m, n)) : (addsmx_nop A :=: A)%MS.

Section AddsmxSub.

-Variable (m1 m2 n : nat) (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)).
+Variable (m1 m2 n : nat) (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)).

-Lemma col_mx_sub m3 (C : 'M_(m3, n)) :
-  (col_mx A B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.
+Lemma col_mx_sub m3 (C : 'M_(m3, n)) :
+  (col_mx A B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.

-Lemma addsmxE : (A + B :=: col_mx A B)%MS.
+Lemma addsmxE : (A + B :=: col_mx A B)%MS.

-Lemma addsmx_sub m3 (C : 'M_(m3, n)) :
-  (A + B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.
+Lemma addsmx_sub m3 (C : 'M_(m3, n)) :
+  (A + B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.

-Lemma addsmxSl : (A ≤ A + B)%MS.
+Lemma addsmxSl : (A ≤ A + B)%MS.

-Lemma addsmxSr : (B ≤ A + B)%MS.
+Lemma addsmxSr : (B ≤ A + B)%MS.

-Lemma addsmx_idPr : reflect (A + B :=: B)%MS (A ≤ B)%MS.
+Lemma addsmx_idPr : reflect (A + B :=: B)%MS (A ≤ B)%MS.

-Lemma addsmx_idPl : reflect (A + B :=: A)%MS (B ≤ A)%MS.
+Lemma addsmx_idPl : reflect (A + B :=: A)%MS (B ≤ A)%MS.

End AddsmxSub.

-Lemma adds0mx m1 m2 n (B : 'M_(m2, n)) : ((0 : 'M_(m1, n)) + B :=: B)%MS.
+Lemma adds0mx m1 m2 n (B : 'M_(m2, n)) : ((0 : 'M_(m1, n)) + B :=: B)%MS.

-Lemma addsmx0 m1 m2 n (A : 'M_(m1, n)) : (A + (0 : 'M_(m2, n)) :=: A)%MS.
+Lemma addsmx0 m1 m2 n (A : 'M_(m1, n)) : (A + (0 : 'M_(m2, n)) :=: A)%MS.

-Let addsmx_nop_eq0 m n (A : 'M_(m, n)) : (addsmx_nop A == 0) = (A == 0).
+Let addsmx_nop_eq0 m n (A : 'M_(m, n)) : (addsmx_nop A == 0) = (A == 0).

-Let addsmx_nop0 m n : addsmx_nop (0 : 'M_(m, n)) = 0.
+Let addsmx_nop0 m n : addsmx_nop (0 : 'M_(m, n)) = 0.

-Let addsmx_nop_id n (A : 'M_n) : addsmx_nop A = A.
+Let addsmx_nop_id n (A : 'M_n) : addsmx_nop A = A.

-Lemma addsmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A + B = B + A)%MS.
+Lemma addsmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A + B = B + A)%MS.

-Lemma adds0mx_id m1 n (B : 'M_n) : ((0 : 'M_(m1, n)) + B)%MS = B.
+Lemma adds0mx_id m1 n (B : 'M_n) : ((0 : 'M_(m1, n)) + B)%MS = B.

-Lemma addsmx0_id m2 n (A : 'M_n) : (A + (0 : 'M_(m2, n)))%MS = A.
+Lemma addsmx0_id m2 n (A : 'M_n) : (A + (0 : 'M_(m2, n)))%MS = A.

-Lemma addsmxA m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A + (B + C) = A + B + C)%MS.
+Lemma addsmxA m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A + (B + C) = A + B + C)%MS.

Canonical addsmx_monoid n :=
@@ -830,230 +829,230 @@ Canonical addsmx_comoid n := Monoid.ComLaw (@addsmxC n n n).

-Lemma addsmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  ((A + B)%MS ×m C :=: A ×m C + B ×m C)%MS.
+Lemma addsmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  ((A + B)%MS ×m C :=: A ×m C + B ×m C)%MS.

-Lemma addsmxS m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
-                            (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
-  (A ≤ C → B ≤ D → A + B ≤ C + D)%MS.
+Lemma addsmxS m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
+                            (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
+  (A ≤ C → B ≤ D → A + B ≤ C + D)%MS.

-Lemma addmx_sub_adds m m1 m2 n (A : 'M_(m, n)) (B : 'M_(m, n))
-                               (C : 'M_(m1, n)) (D : 'M_(m2, n)) :
-  (A ≤ C → B ≤ D → (A + B)%R ≤ C + D)%MS.
+Lemma addmx_sub_adds m m1 m2 n (A : 'M_(m, n)) (B : 'M_(m, n))
+                               (C : 'M_(m1, n)) (D : 'M_(m2, n)) :
+  (A ≤ C → B ≤ D → (A + B)%R ≤ C + D)%MS.

-Lemma addsmx_addKl n m1 m2 (A : 'M_(m1, n)) (B C : 'M_(m2, n)) :
-  (B ≤ A)%MS → (A + (B + C)%R :=: A + C)%MS.
+Lemma addsmx_addKl n m1 m2 (A : 'M_(m1, n)) (B C : 'M_(m2, n)) :
+  (B ≤ A)%MS → (A + (B + C)%R :=: A + C)%MS.

-Lemma addsmx_addKr n m1 m2 (A B : 'M_(m1, n)) (C : 'M_(m2, n)) :
-  (B ≤ C)%MS → ((A + B)%R + C :=: A + C)%MS.
+Lemma addsmx_addKr n m1 m2 (A B : 'M_(m1, n)) (C : 'M_(m2, n)) :
+  (B ≤ C)%MS → ((A + B)%R + C :=: A + C)%MS.

-Lemma adds_eqmx m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
-                              (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
-  (A :=: C → B :=: D → A + B :=: C + D)%MS.
+Lemma adds_eqmx m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
+                              (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
+  (A :=: C → B :=: D → A + B :=: C + D)%MS.

-Lemma genmx_adds m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (<<(A + B)%MS>> = <<A>> + <<B>>)%MS.
+Lemma genmx_adds m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (<<(A + B)%MS>> = <<A>> + <<B>>)%MS.

Lemma sub_addsmxP m1 m2 m3 n
-                  (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  reflect (∃ u, A = u.1 ×m B + u.2 ×m C) (A ≤ B + C)%MS.
+                  (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  reflect (∃ u, A = u.1 ×m B + u.2 ×m C) (A ≤ B + C)%MS.

Variable I : finType.
-Implicit Type P : pred I.
+Implicit Type P : pred I.

-Lemma genmx_sums P n (B_ : I → 'M_n) :
-  <<(\sum_(i | P i) B_ i)%MS>>%MS = (\sum_(i | P i) <<B_ i>>)%MS.
+Lemma genmx_sums P n (B_ : I → 'M_n) :
+  <<(\sum_(i | P i) B_ i)%MS>>%MS = (\sum_(i | P i) <<B_ i>>)%MS.

-Lemma sumsmx_sup i0 P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
-  P i0 → (A ≤ B_ i0)%MS → (A ≤ \sum_(i | P i) B_ i)%MS.
+Lemma sumsmx_sup i0 P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
+  P i0 → (A ≤ B_ i0)%MS → (A ≤ \sum_(i | P i) B_ i)%MS.

-Lemma sumsmx_subP P m n (A_ : I → 'M_n) (B : 'M_(m, n)) :
-  reflect (∀ i, P i → A_ i ≤ B)%MS (\sum_(i | P i) A_ i ≤ B)%MS.
+Lemma sumsmx_subP P m n (A_ : I → 'M_n) (B : 'M_(m, n)) :
+  reflect (∀ i, P i → A_ i ≤ B)%MS (\sum_(i | P i) A_ i ≤ B)%MS.

-Lemma summx_sub_sums P m n (A : I → 'M[F]_(m, n)) B :
-    (∀ i, P i → A i ≤ B i)%MS →
-  ((\sum_(i | P i) A i)%R ≤ \sum_(i | P i) B i)%MS.
+Lemma summx_sub_sums P m n (A : I → 'M[F]_(m, n)) B :
+    (∀ i, P i → A i ≤ B i)%MS →
+  ((\sum_(i | P i) A i)%R ≤ \sum_(i | P i) B i)%MS.

-Lemma sumsmxS P n (A B : I → 'M[F]_n) :
-    (∀ i, P i → A i ≤ B i)%MS →
-  (\sum_(i | P i) A i ≤ \sum_(i | P i) B i)%MS.
+Lemma sumsmxS P n (A B : I → 'M[F]_n) :
+    (∀ i, P i → A i ≤ B i)%MS →
+  (\sum_(i | P i) A i ≤ \sum_(i | P i) B i)%MS.

-Lemma eqmx_sums P n (A B : I → 'M[F]_n) :
-    (∀ i, P i → A i :=: B i)%MS →
-  (\sum_(i | P i) A i :=: \sum_(i | P i) B i)%MS.
+Lemma eqmx_sums P n (A B : I → 'M[F]_n) :
+    (∀ i, P i → A i :=: B i)%MS →
+  (\sum_(i | P i) A i :=: \sum_(i | P i) B i)%MS.

-Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
-  reflect (∃ u_, A = \sum_(i | P i) u_ i ×m B_ i)
-          (A ≤ \sum_(i | P i) B_ i)%MS.
+Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
+  reflect (∃ u_, A = \sum_(i | P i) u_ i ×m B_ i)
+          (A ≤ \sum_(i | P i) B_ i)%MS.

-Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) :
-  ((\sum_(i | P i) A i)%MS ×m B :=: \sum_(i | P i) <<A i ×m B>>)%MS.
+Lemma sumsmxMr_gen P m n A (B : 'M[F]_(m, n)) :
+  ((\sum_(i | P i) A i)%MS ×m B :=: \sum_(i | P i) <<A i ×m B>>)%MS.

-Lemma sumsmxMr P n (A_ : I → 'M[F]_n) (B : 'M_n) :
-  ((\sum_(i | P i) A_ i)%MS ×m B :=: \sum_(i | P i) (A_ i ×m B))%MS.
+Lemma sumsmxMr P n (A_ : I → 'M[F]_n) (B : 'M_n) :
+  ((\sum_(i | P i) A_ i)%MS ×m B :=: \sum_(i | P i) (A_ i ×m B))%MS.

-Lemma rank_pid_mx m n r : r ≤ m → r ≤ n → \rank (pid_mx r : 'M_(m, n)) = r.
+Lemma rank_pid_mx m n r : r ≤ m → r ≤ n → \rank (pid_mx r : 'M_(m, n)) = r.

-Lemma rank_copid_mx n r : r ≤ n → \rank (copid_mx r : 'M_n) = (n - r)%N.
+Lemma rank_copid_mx n r : r ≤ n → \rank (copid_mx r : 'M_n) = (n - r)%N.

-Lemma mxrank_compl m n (A : 'M_(m, n)) : \rank A^C = (n - \rank A)%N.
+Lemma mxrank_compl m n (A : 'M_(m, n)) : \rank A^C = (n - \rank A)%N.

-Lemma mxrank_ker m n (A : 'M_(m, n)) : \rank (kermx A) = (m - \rank A)%N.
+Lemma mxrank_ker m n (A : 'M_(m, n)) : \rank (kermx A) = (m - \rank A)%N.

-Lemma kermx_eq0 n m (A : 'M_(m, n)) : (kermx A == 0) = row_free A.
+Lemma kermx_eq0 n m (A : 'M_(m, n)) : (kermx A == 0) = row_free A.

-Lemma mxrank_coker m n (A : 'M_(m, n)) : \rank (cokermx A) = (n - \rank A)%N.
+Lemma mxrank_coker m n (A : 'M_(m, n)) : \rank (cokermx A) = (n - \rank A)%N.

-Lemma cokermx_eq0 n m (A : 'M_(m, n)) : (cokermx A == 0) = row_full A.
+Lemma cokermx_eq0 n m (A : 'M_(m, n)) : (cokermx A == 0) = row_full A.

-Lemma mulmx_ker m n (A : 'M_(m, n)) : kermx A ×m A = 0.
+Lemma mulmx_ker m n (A : 'M_(m, n)) : kermx A ×m A = 0.

-Lemma mulmxKV_ker m n p (A : 'M_(n, p)) (B : 'M_(m, n)) :
-  B ×m A = 0 → B ×m col_ebase A ×m kermx A = B.
+Lemma mulmxKV_ker m n p (A : 'M_(n, p)) (B : 'M_(m, n)) :
+  B ×m A = 0 → B ×m col_ebase A ×m kermx A = B.

-Lemma sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
-  reflect (B ×m A = 0) (B ≤ kermx A)%MS.
+Lemma sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
+  reflect (B ×m A = 0) (B ≤ kermx A)%MS.

-Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  A ×m B = 0 → \rank A + \rank B ≤ n.
+Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  A ×m B = 0 → \rank A + \rank B ≤ n.

-Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) :
-  \rank (A ×m B) + \rank (B ×m C) ≤ \rank B + \rank (A ×m B ×m C).
+Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) :
+  \rank (A ×m B) + \rank (B ×m C) ≤ \rank B + \rank (A ×m B ×m C).

-Lemma mxrank_mul_min m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  \rank A + \rank B - n ≤ \rank (A ×m B).
+Lemma mxrank_mul_min m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  \rank A + \rank B - n ≤ \rank (A ×m B).

-Lemma addsmx_compl_full m n (A : 'M_(m, n)) : row_full (A + A^C)%MS.
+Lemma addsmx_compl_full m n (A : 'M_(m, n)) : row_full (A + A^C)%MS.

-Lemma sub_capmx_gen m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A ≤ capmx_gen B C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.
+Lemma sub_capmx_gen m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A ≤ capmx_gen B C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.

-Let capmx_witnessP m n (A : 'M_(m, n)) : equivmx A (qidmx A) (capmx_witness A).
+Let capmx_witnessP m n (A : 'M_(m, n)) : equivmx A (qidmx A) (capmx_witness A).

-Let capmx_normP m n (A : 'M_(m, n)) : equivmx_spec A (qidmx A) (capmx_norm A).
+Let capmx_normP m n (A : 'M_(m, n)) : equivmx_spec A (qidmx A) (capmx_norm A).

-Let capmx_norm_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  qidmx A = qidmx B → (A == B)%MS → capmx_norm A = capmx_norm B.
+Let capmx_norm_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  qidmx A = qidmx B → (A == B)%MS → capmx_norm A = capmx_norm B.

-Let capmx_nopP m n (A : 'M_(m, n)) : equivmx_spec A (qidmx A) (capmx_nop A).
+Let capmx_nopP m n (A : 'M_(m, n)) : equivmx_spec A (qidmx A) (capmx_nop A).

-Let sub_qidmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  qidmx B → (A ≤ B)%MS.
+Let sub_qidmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  qidmx B → (A ≤ B)%MS.

-Let qidmx_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  qidmx (A :&: B)%MS = qidmx A && qidmx B.
+Let qidmx_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  qidmx (A :&: B)%MS = qidmx A && qidmx B.

-Let capmx_eq_norm m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  qidmx A = qidmx B → (A :&: B)%MS = capmx_norm (A :&: B)%MS.
+Let capmx_eq_norm m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  qidmx A = qidmx B → (A :&: B)%MS = capmx_norm (A :&: B)%MS.

-Lemma capmxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :&: B :=: capmx_gen A B)%MS.
+Lemma capmxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :&: B :=: capmx_gen A B)%MS.

-Lemma capmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B ≤ A)%MS.
+Lemma capmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B ≤ A)%MS.

-Lemma sub_capmx m m1 m2 n (A : 'M_(m, n)) (B : 'M_(m1, n)) (C : 'M_(m2, n)) :
-  (A ≤ B :&: C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.
+Lemma sub_capmx m m1 m2 n (A : 'M_(m, n)) (B : 'M_(m1, n)) (C : 'M_(m2, n)) :
+  (A ≤ B :&: C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.

-Lemma capmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B = B :&: A)%MS.
+Lemma capmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B = B :&: A)%MS.

-Lemma capmxSr m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B ≤ B)%MS.
+Lemma capmxSr m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B ≤ B)%MS.

-Lemma capmx_idPr n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (A :&: B :=: B)%MS (B ≤ A)%MS.
+Lemma capmx_idPr n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (A :&: B :=: B)%MS (B ≤ A)%MS.

-Lemma capmx_idPl n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (A :&: B :=: A)%MS (A ≤ B)%MS.
+Lemma capmx_idPl n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (A :&: B :=: A)%MS (A ≤ B)%MS.

-Lemma capmxS m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
-                           (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
-  (A ≤ C → B ≤ D → A :&: B ≤ C :&: D)%MS.
+Lemma capmxS m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
+                           (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
+  (A ≤ C → B ≤ D → A :&: B ≤ C :&: D)%MS.

-Lemma cap_eqmx m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
-                             (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
-  (A :=: C → B :=: D → A :&: B :=: C :&: D)%MS.
+Lemma cap_eqmx m1 m2 m3 m4 n (A : 'M_(m1, n)) (B : 'M_(m2, n))
+                             (C : 'M_(m3, n)) (D : 'M_(m4, n)) :
+  (A :=: C → B :=: D → A :&: B :=: C :&: D)%MS.

-Lemma capmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
-  ((A :&: B) ×m C ≤ A ×m C :&: B ×m C)%MS.
+Lemma capmxMr m1 m2 n p (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)) :
+  ((A :&: B) ×m C ≤ A ×m C :&: B ×m C)%MS.

-Lemma cap0mx m1 m2 n (A : 'M_(m2, n)) : ((0 : 'M_(m1, n)) :&: A)%MS = 0.
+Lemma cap0mx m1 m2 n (A : 'M_(m2, n)) : ((0 : 'M_(m1, n)) :&: A)%MS = 0.

-Lemma capmx0 m1 m2 n (A : 'M_(m1, n)) : (A :&: (0 : 'M_(m2, n)))%MS = 0.
+Lemma capmx0 m1 m2 n (A : 'M_(m1, n)) : (A :&: (0 : 'M_(m2, n)))%MS = 0.

-Lemma capmxT m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  row_full B → (A :&: B :=: A)%MS.
+Lemma capmxT m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  row_full B → (A :&: B :=: A)%MS.

-Lemma capTmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  row_full A → (A :&: B :=: B)%MS.
+Lemma capTmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  row_full A → (A :&: B :=: B)%MS.

-Let capmx_nop_id n (A : 'M_n) : capmx_nop A = A.
+Let capmx_nop_id n (A : 'M_n) : capmx_nop A = A.

-Lemma cap1mx n (A : 'M_n) : (1%:M :&: A = A)%MS.
+Lemma cap1mx n (A : 'M_n) : (1%:M :&: A = A)%MS.

-Lemma capmx1 n (A : 'M_n) : (A :&: 1%:M = A)%MS.
+Lemma capmx1 n (A : 'M_n) : (A :&: 1%:M = A)%MS.

-Lemma genmx_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  <<A :&: B>>%MS = (<<A>> :&: <<B>>)%MS.
+Lemma genmx_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  <<A :&: B>>%MS = (<<A>> :&: <<B>>)%MS.

-Lemma capmxA m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A :&: (B :&: C) = A :&: B :&: C)%MS.
+Lemma capmxA m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A :&: (B :&: C) = A :&: B :&: C)%MS.

Canonical capmx_monoid n :=
@@ -1061,70 +1060,70 @@ Canonical capmx_comoid n := Monoid.ComLaw (@capmxC n n n).

-Lemma bigcapmx_inf i0 P m n (A_ : I → 'M_n) (B : 'M_(m, n)) :
-  P i0 → (A_ i0 ≤ B → \bigcap_(i | P i) A_ i ≤ B)%MS.
+Lemma bigcapmx_inf i0 P m n (A_ : I → 'M_n) (B : 'M_(m, n)) :
+  P i0 → (A_ i0 ≤ B → \bigcap_(i | P i) A_ i ≤ B)%MS.

-Lemma sub_bigcapmxP P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
-  reflect (∀ i, P i → A ≤ B_ i)%MS (A ≤ \bigcap_(i | P i) B_ i)%MS.
+Lemma sub_bigcapmxP P m n (A : 'M_(m, n)) (B_ : I → 'M_n) :
+  reflect (∀ i, P i → A ≤ B_ i)%MS (A ≤ \bigcap_(i | P i) B_ i)%MS.

-Lemma genmx_bigcap P n (A_ : I → 'M_n) :
-  (<<\bigcap_(i | P i) A_ i>> = \bigcap_(i | P i) <<A_ i>>)%MS.
+Lemma genmx_bigcap P n (A_ : I → 'M_n) :
+  (<<\bigcap_(i | P i) A_ i>> = \bigcap_(i | P i) <<A_ i>>)%MS.

-Lemma matrix_modl m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (A ≤ C → A + (B :&: C) :=: (A + B) :&: C)%MS.
+Lemma matrix_modl m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (A ≤ C → A + (B :&: C) :=: (A + B) :&: C)%MS.

-Lemma matrix_modr m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
-  (C ≤ A → (A :&: B) + C :=: A :&: (B + C))%MS.
+Lemma matrix_modr m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) :
+  (C ≤ A → (A :&: B) + C :=: A :&: (B + C))%MS.

-Lemma capmx_compl m n (A : 'M_(m, n)) : (A :&: A^C)%MS = 0.
+Lemma capmx_compl m n (A : 'M_(m, n)) : (A :&: A^C)%MS = 0.

-Lemma mxrank_mul_ker m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
-  (\rank (A ×m B) + \rank (A :&: kermx B))%N = \rank A.
+Lemma mxrank_mul_ker m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
+  (\rank (A ×m B) + \rank (A :&: kermx B))%N = \rank A.

-Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) :
-  reflect (\rank (A ×m f) = \rank A) ((A :&: kermx f)%MS == 0).
+Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) :
+  reflect (\rank (A ×m f) = \rank A) ((A :&: kermx f)%MS == 0).

-Lemma mxrank_disjoint_sum m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :&: B)%MS = 0 → \rank (A + B)%MS = (\rank A + \rank B)%N.
+Lemma mxrank_disjoint_sum m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :&: B)%MS = 0 → \rank (A + B)%MS = (\rank A + \rank B)%N.

-Lemma diffmxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :\: B :=: A :&: (capmx_gen A B)^C)%MS.
+Lemma diffmxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :\: B :=: A :&: (capmx_gen A B)^C)%MS.

-Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (<<A :\: B>> = A :\: B)%MS.
+Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (<<A :\: B>> = A :\: B)%MS.

-Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B ≤ A)%MS.
+Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B ≤ A)%MS.

-Lemma capmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  ((A :\: B) :&: B)%MS = 0.
+Lemma capmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  ((A :\: B) :&: B)%MS = 0.

-Lemma addsmx_diff_cap_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A :\: B + A :&: B :=: A)%MS.
+Lemma addsmx_diff_cap_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :\: B + A :&: B :=: A)%MS.

-Lemma mxrank_cap_compl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (\rank (A :&: B) + \rank (A :\: B))%N = \rank A.
+Lemma mxrank_cap_compl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (\rank (A :&: B) + \rank (A :\: B))%N = \rank A.

-Lemma mxrank_sum_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (\rank (A + B) + \rank (A :&: B) = \rank A + \rank B)%N.
+Lemma mxrank_sum_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (\rank (A + B) + \rank (A :&: B) = \rank A + \rank B)%N.

-Lemma mxrank_adds_leqif m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  \rank (A + B) ≤ \rank A + \rank B ?= iff (A :&: B ≤ (0 : 'M_n))%MS.
+Lemma mxrank_adds_leqif m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  \rank (A + B) ≤ \rank A + \rank B ?= iff (A :&: B ≤ (0 : 'M_n))%MS.

@@ -1135,28 +1134,28 @@

-Lemma proj_mx_sub m n U V (W : 'M_(m, n)) : (W ×m proj_mx U V ≤ U)%MS.
+Lemma proj_mx_sub m n U V (W : 'M_(m, n)) : (W ×m proj_mx U V ≤ U)%MS.

-Lemma proj_mx_compl_sub m n U V (W : 'M_(m, n)) :
-  (W ≤ U + V → W - W ×m proj_mx U V ≤ V)%MS.
+Lemma proj_mx_compl_sub m n U V (W : 'M_(m, n)) :
+  (W ≤ U + V → W - W ×m proj_mx U V ≤ V)%MS.

-Lemma proj_mx_id m n U V (W : 'M_(m, n)) :
-  (U :&: V = 0)%MS → (W ≤ U)%MS → W ×m proj_mx U V = W.
+Lemma proj_mx_id m n U V (W : 'M_(m, n)) :
+  (U :&: V = 0)%MS → (W ≤ U)%MS → W ×m proj_mx U V = W.

-Lemma proj_mx_0 m n U V (W : 'M_(m, n)) :
-  (U :&: V = 0)%MS → (W ≤ V)%MS → W ×m proj_mx U V = 0.
+Lemma proj_mx_0 m n U V (W : 'M_(m, n)) :
+  (U :&: V = 0)%MS → (W ≤ V)%MS → W ×m proj_mx U V = 0.

-Lemma add_proj_mx m n U V (W : 'M_(m, n)) :
-    (U :&: V = 0)%MS → (W ≤ U + V)%MS →
-  W ×m proj_mx U V + W ×m proj_mx V U = W.
+Lemma add_proj_mx m n U V (W : 'M_(m, n)) :
+    (U :&: V = 0)%MS → (W ≤ U + V)%MS →
+  W ×m proj_mx U V + W ×m proj_mx V U = W.

-Lemma proj_mx_proj n (U V : 'M_n) :
-  let P := proj_mx U V in (U :&: V = 0)%MS → P ×m P = P.
+Lemma proj_mx_proj n (U V : 'M_n) :
+  let P := proj_mx U V in (U :&: V = 0)%MS → P ×m P = P.

@@ -1167,8 +1166,21 @@

-Lemma complete_unitmx m n (U : 'M_(m, n)) (f : 'M_n) :
-  \rank (U ×m f) = \rank U → {g : 'M_n | g \in unitmx & U ×m f = U ×m g}.
+Lemma complete_unitmx m n (U : 'M_(m, n)) (f : 'M_n) :
+  \rank (U ×m f) = \rank U → {g : 'M_n | g \in unitmx & U ×m f = U ×m g}.
+ +
+
+ +
+ Two matrices with the same shape represent the same subspace + iff they differ only by a change of basis. +
+
+ +
+Lemma eqmxMunitP m n (U V : 'M_(m, n)) :
+  reflect (exists2 P, P \in unitmx & U = P ×m V) (U == V)%MS.

@@ -1179,8 +1191,8 @@

-Lemma eq_rank_unitmx m1 m2 n (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
-  \rank U = \rank V → {f : 'M_n | f \in unitmx & V :=: U ×m f}%MS.
+Lemma eq_rank_unitmx m1 m2 n (U : 'M_(m1, n)) (V : 'M_(m2, n)) :
+  \rank U = \rank V → {f : 'M_n | f \in unitmx & V :=: U ×m f}%MS.

Section SumExpr.
@@ -1292,28 +1304,28 @@

-Inductive mxsum_spec n : ∀ m, 'M[F]_(m, n) → nat → Prop :=
+Inductive mxsum_spec n : ∀ m, 'M[F]_(m, n) → nat → Prop :=
 | TrivialMxsum m A
-    : @mxsum_spec n m A (\rank A)
+    : @mxsum_spec n m A (\rank A)
 | ProperMxsum m1 m2 T1 T2 r1 r2 of
      @mxsum_spec n m1 T1 r1 & @mxsum_spec n m2 T2 r2
-    : mxsum_spec (T1 + T2)%MS (r1 + r2)%N.
+    : mxsum_spec (T1 + T2)%MS (r1 + r2)%N.

Structure mxsum_expr m n := Mxsum {
-  mxsum_val :> wrapped 'M_(m, n);
-  mxsum_rank : wrapped nat;
-  _ : mxsum_spec (unwrap mxsum_val) (unwrap mxsum_rank)
+  mxsum_val :> wrapped 'M_(m, n);
+  mxsum_rank : wrapped nat;
+  _ : mxsum_spec (unwrap mxsum_val) (unwrap mxsum_rank)
}.

Canonical trivial_mxsum m n A :=
-  @Mxsum m n (Wrap A) (Wrap (\rank A)) (TrivialMxsum A).
+  @Mxsum m n (Wrap A) (Wrap (\rank A)) (TrivialMxsum A).

Structure proper_mxsum_expr n := ProperMxsumExpr {
-  proper_mxsum_val :> 'M_n;
-  proper_mxsum_rank : nat;
+  proper_mxsum_val :> 'M_n;
+  proper_mxsum_rank : nat;
  _ : mxsum_spec proper_mxsum_val proper_mxsum_rank
}.
@@ -1324,70 +1336,70 @@
Canonical sum_mxsum n (S : proper_mxsum_expr n) :=
-  @Mxsum n n (wrap (S : 'M_n)) (wrap (proper_mxsum_rank S)) (proper_mxsumP S).
+  @Mxsum n n (wrap (S : 'M_n)) (wrap (proper_mxsum_rank S)) (proper_mxsumP S).

Section Binary.
-Variable (m1 m2 n : nat) (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n).
+Variable (m1 m2 n : nat) (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n).
Fact binary_mxsum_proof :
-  mxsum_spec (unwrap S1 + unwrap S2)
-             (unwrap (mxsum_rank S1) + unwrap (mxsum_rank S2)).
+  mxsum_spec (unwrap S1 + unwrap S2)
+             (unwrap (mxsum_rank S1) + unwrap (mxsum_rank S2)).
Canonical binary_mxsum_expr := ProperMxsumExpr binary_mxsum_proof.
End Binary.

Section Nary.
-Context J (r : seq J) (P : pred J) n (S_ : J → mxsum_expr n n).
+Context J (r : seq J) (P : pred J) n (S_ : J → mxsum_expr n n).
Fact nary_mxsum_proof :
-  mxsum_spec (\sum_(j <- r | P j) unwrap (S_ j))
-             (\sum_(j <- r | P j) unwrap (mxsum_rank (S_ j))).
+  mxsum_spec (\sum_(j <- r | P j) unwrap (S_ j))
+             (\sum_(j <- r | P j) unwrap (mxsum_rank (S_ j))).
Canonical nary_mxsum_expr := ProperMxsumExpr nary_mxsum_proof.
End Nary.

-Definition mxdirect_def m n T of phantom 'M_(m, n) (unwrap (mxsum_val T)) :=
-  \rank (unwrap T) == unwrap (mxsum_rank T).
+Definition mxdirect_def m n T of phantom 'M_(m, n) (unwrap (mxsum_val T)) :=
+  \rank (unwrap T) == unwrap (mxsum_rank T).

End SumExpr.

-Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)).
+Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)).

Lemma mxdirectP n (S : proper_mxsum_expr n) :
-  reflect (\rank S = proper_mxsum_rank S) (mxdirect S).
+  reflect (\rank S = proper_mxsum_rank S) (mxdirect S).

-Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)).
+Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)).

Lemma mxrank_sum_leqif m n (S : mxsum_expr m n) :
-  \rank (unwrap S) ≤ unwrap (mxsum_rank S) ?= iff mxdirect (unwrap S).
+  \rank (unwrap S) ≤ unwrap (mxsum_rank S) ?= iff mxdirect (unwrap S).

Lemma mxdirectE m n (S : mxsum_expr m n) :
-  mxdirect (unwrap S) = (\rank (unwrap S) == unwrap (mxsum_rank S)).
+  mxdirect (unwrap S) = (\rank (unwrap S) == unwrap (mxsum_rank S)).

Lemma mxdirectEgeq m n (S : mxsum_expr m n) :
-  mxdirect (unwrap S) = (\rank (unwrap S) ≥ unwrap (mxsum_rank S)).
+  mxdirect (unwrap S) = (\rank (unwrap S) ≥ unwrap (mxsum_rank S)).

Section BinaryDirect.

-Variables m1 m2 n : nat.
+Variables m1 m2 n : nat.

Lemma mxdirect_addsE (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n) :
-   mxdirect (unwrap S1 + unwrap S2)
-    = [&& mxdirect (unwrap S1), mxdirect (unwrap S2)
-        & unwrap S1 :&: unwrap S2 == 0]%MS.
+   mxdirect (unwrap S1 + unwrap S2)
+    = [&& mxdirect (unwrap S1), mxdirect (unwrap S2)
+        & unwrap S1 :&: unwrap S2 == 0]%MS.

-Lemma mxdirect_addsP (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  reflect (A :&: B = 0)%MS (mxdirect (A + B)).
+Lemma mxdirect_addsP (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  reflect (A :&: B = 0)%MS (mxdirect (A + B)).

End BinaryDirect.
@@ -1396,26 +1408,26 @@ Section NaryDirect.

-Variables (P : pred I) (n : nat).
+Variables (P : pred I) (n : nat).

-Let TIsum A_ i := (A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0 :> 'M_n)%MS.
+Let TIsum A_ i := (A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0 :> 'M_n)%MS.

-Let mxdirect_sums_recP (S_ : I → mxsum_expr n n) :
-  reflect (∀ i, P i → mxdirect (unwrap (S_ i)) ∧ TIsum (unwrap \o S_) i)
-          (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).
+Let mxdirect_sums_recP (S_ : I → mxsum_expr n n) :
+  reflect (∀ i, P i → mxdirect (unwrap (S_ i)) ∧ TIsum (unwrap \o S_) i)
+          (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).

-Lemma mxdirect_sumsP (A_ : I → 'M_n) :
-  reflect (∀ i, P i → A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0)%MS
-          (mxdirect (\sum_(i | P i) A_ i)).
+Lemma mxdirect_sumsP (A_ : I → 'M_n) :
+  reflect (∀ i, P i → A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0)%MS
+          (mxdirect (\sum_(i | P i) A_ i)).

-Lemma mxdirect_sumsE (S_ : I → mxsum_expr n n) (xunwrap := unwrap) :
-  reflect (and (∀ i, P i → mxdirect (unwrap (S_ i)))
-               (mxdirect (\sum_(i | P i) (xunwrap (S_ i)))))
-          (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).
+Lemma mxdirect_sumsE (S_ : I → mxsum_expr n n) (xunwrap := unwrap) :
+  reflect (and (∀ i, P i → mxdirect (unwrap (S_ i)))
+               (mxdirect (\sum_(i | P i) (xunwrap (S_ i)))))
+          (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).

End NaryDirect.
@@ -1424,17 +1436,17 @@ Section SubDaddsmx.

-Variables m m1 m2 n : nat.
-Variables (A : 'M[F]_(m, n)) (B1 : 'M[F]_(m1, n)) (B2 : 'M[F]_(m2, n)).
+Variables m m1 m2 n : nat.
+Variables (A : 'M[F]_(m, n)) (B1 : 'M[F]_(m1, n)) (B2 : 'M[F]_(m2, n)).

-CoInductive sub_daddsmx_spec : Prop :=
-  SubDaddsmxSpec A1 A2 of (A1 ≤ B1)%MS & (A2 ≤ B2)%MS & A = A1 + A2
-                        & ∀ C1 C2, (C1 ≤ B1)%MS → (C2 ≤ B2)%MS →
-                          A = C1 + C2 → C1 = A1 ∧ C2 = A2.
+Variant sub_daddsmx_spec : Prop :=
+  SubDaddsmxSpec A1 A2 of (A1 ≤ B1)%MS & (A2 ≤ B2)%MS & A = A1 + A2
+                        & ∀ C1 C2, (C1 ≤ B1)%MS → (C2 ≤ B2)%MS →
+                          A = C1 + C2 → C1 = A1 ∧ C2 = A2.

-Lemma sub_daddsmx : (B1 :&: B2 = 0)%MS → (A ≤ B1 + B2)%MS → sub_daddsmx_spec.
+Lemma sub_daddsmx : (B1 :&: B2 = 0)%MS → (A ≤ B1 + B2)%MS → sub_daddsmx_spec.

End SubDaddsmx.
@@ -1443,18 +1455,18 @@ Section SubDsumsmx.

-Variables (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B : I → 'M[F]_n).
+Variables (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B : I → 'M[F]_n).

-CoInductive sub_dsumsmx_spec : Prop :=
-  SubDsumsmxSpec A_ of ∀ i, P i → (A_ i ≤ B i)%MS
-                        & A = \sum_(i | P i) A_ i
-                        & ∀ C, (∀ i, P i → C i ≤ B i)%MS →
-                          A = \sum_(i | P i) C i → {in SimplPred P, C =1 A_}.
+Variant sub_dsumsmx_spec : Prop :=
+  SubDsumsmxSpec A_ of ∀ i, P i → (A_ i ≤ B i)%MS
+                        & A = \sum_(i | P i) A_ i
+                        & ∀ C, (∀ i, P i → C i ≤ B i)%MS →
+                          A = \sum_(i | P i) C i → {in SimplPred P, C =1 A_}.

Lemma sub_dsumsmx :
-    mxdirect (\sum_(i | P i) B i) → (A ≤ \sum_(i | P i) B i)%MS →
+    mxdirect (\sum_(i | P i) B i) → (A ≤ \sum_(i | P i) B i)%MS →
  sub_dsumsmx_spec.

@@ -1464,23 +1476,23 @@ Section Eigenspace.

-Variables (n : nat) (g : 'M_n).
+Variables (n : nat) (g : 'M_n).

-Definition eigenspace a := kermx (g - a%:M).
-Definition eigenvalue : pred F := fun a ⇒ eigenspace a != 0.
+Definition eigenspace a := kermx (g - a%:M).
+Definition eigenvalue : pred F := fun a ⇒ eigenspace a != 0.

-Lemma eigenspaceP a m (W : 'M_(m, n)) :
-  reflect (W ×m g = a *: W) (W ≤ eigenspace a)%MS.
+Lemma eigenspaceP a m (W : 'M_(m, n)) :
+  reflect (W ×m g = a *: W) (W ≤ eigenspace a)%MS.

Lemma eigenvalueP a :
-  reflect (exists2 v : 'rV_n, v ×m g = a *: v & v != 0) (eigenvalue a).
+  reflect (exists2 v : 'rV_n, v ×m g = a *: v & v != 0) (eigenvalue a).

-Lemma mxdirect_sum_eigenspace (P : pred I) a_ :
-  {in P &, injective a_} → mxdirect (\sum_(i | P i) eigenspace (a_ i)).
+Lemma mxdirect_sum_eigenspace (P : pred I) a_ :
+  {in P &, injective a_} → mxdirect (\sum_(i | P i) eigenspace (a_ i)).

End Eigenspace.
@@ -1489,84 +1501,84 @@ End RowSpaceTheory.

-Hint Resolve submx_refl.
- -
-Notation "\rank A" := (mxrank A) : nat_scope.
-Notation "<< A >>" := (genmx A) : matrix_set_scope.
-Notation "A ^C" := (complmx A) : matrix_set_scope.
-Notation "A <= B" := (submx A B) : matrix_set_scope.
-Notation "A < B" := (ltmx A B) : matrix_set_scope.
-Notation "A <= B <= C" := ((submx A B) && (submx B C)) : matrix_set_scope.
-Notation "A < B <= C" := (ltmx A B && submx B C) : matrix_set_scope.
-Notation "A <= B < C" := (submx A B && ltmx B C) : matrix_set_scope.
-Notation "A < B < C" := (ltmx A B && ltmx B C) : matrix_set_scope.
-Notation "A == B" := ((submx A B) && (submx B A)) : matrix_set_scope.
-Notation "A :=: B" := (eqmx A B) : matrix_set_scope.
-Notation "A + B" := (addsmx A B) : matrix_set_scope.
-Notation "A :&: B" := (capmx A B) : matrix_set_scope.
-Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
-Notation mxdirect S := (mxdirect_def (Phantom 'M_(_,_) S%MS)).
- -
-Notation "\sum_ ( i <- r | P ) B" :=
-  (\big[addsmx/0%R]_(i <- r | P%B) B%MS) : matrix_set_scope.
-Notation "\sum_ ( i <- r ) B" :=
-  (\big[addsmx/0%R]_(i <- r) B%MS) : matrix_set_scope.
-Notation "\sum_ ( m <= i < n | P ) B" :=
-  (\big[addsmx/0%R]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
-Notation "\sum_ ( m <= i < n ) B" :=
-  (\big[addsmx/0%R]_(m ≤ i < n) B%MS) : matrix_set_scope.
-Notation "\sum_ ( i | P ) B" :=
-  (\big[addsmx/0%R]_(i | P%B) B%MS) : matrix_set_scope.
-Notation "\sum_ i B" :=
-  (\big[addsmx/0%R]_i B%MS) : matrix_set_scope.
-Notation "\sum_ ( i : t | P ) B" :=
-  (\big[addsmx/0%R]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
-Notation "\sum_ ( i : t ) B" :=
-  (\big[addsmx/0%R]_(i : t) B%MS) (only parsing) : matrix_set_scope.
-Notation "\sum_ ( i < n | P ) B" :=
-  (\big[addsmx/0%R]_(i < n | P%B) B%MS) : matrix_set_scope.
-Notation "\sum_ ( i < n ) B" :=
-  (\big[addsmx/0%R]_(i < n) B%MS) : matrix_set_scope.
-Notation "\sum_ ( i 'in' A | P ) B" :=
-  (\big[addsmx/0%R]_(i in A | P%B) B%MS) : matrix_set_scope.
-Notation "\sum_ ( i 'in' A ) B" :=
-  (\big[addsmx/0%R]_(i in A) B%MS) : matrix_set_scope.
- -
-Notation "\bigcap_ ( i <- r | P ) B" :=
-  (\big[capmx/1%:M]_(i <- r | P%B) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i <- r ) B" :=
-  (\big[capmx/1%:M]_(i <- r) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( m <= i < n | P ) B" :=
-  (\big[capmx/1%:M]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( m <= i < n ) B" :=
-  (\big[capmx/1%:M]_(m ≤ i < n) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i | P ) B" :=
-  (\big[capmx/1%:M]_(i | P%B) B%MS) : matrix_set_scope.
-Notation "\bigcap_ i B" :=
-  (\big[capmx/1%:M]_i B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i : t | P ) B" :=
-  (\big[capmx/1%:M]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
-Notation "\bigcap_ ( i : t ) B" :=
-  (\big[capmx/1%:M]_(i : t) B%MS) (only parsing) : matrix_set_scope.
-Notation "\bigcap_ ( i < n | P ) B" :=
-  (\big[capmx/1%:M]_(i < n | P%B) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i < n ) B" :=
-  (\big[capmx/1%:M]_(i < n) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i 'in' A | P ) B" :=
-  (\big[capmx/1%:M]_(i in A | P%B) B%MS) : matrix_set_scope.
-Notation "\bigcap_ ( i 'in' A ) B" :=
-  (\big[capmx/1%:M]_(i in A) B%MS) : matrix_set_scope.
+Hint Resolve submx_refl : core.
+ +
+Notation "\rank A" := (mxrank A) : nat_scope.
+Notation "<< A >>" := (genmx A) : matrix_set_scope.
+Notation "A ^C" := (complmx A) : matrix_set_scope.
+Notation "A <= B" := (submx A B) : matrix_set_scope.
+Notation "A < B" := (ltmx A B) : matrix_set_scope.
+Notation "A <= B <= C" := ((submx A B) && (submx B C)) : matrix_set_scope.
+Notation "A < B <= C" := (ltmx A B && submx B C) : matrix_set_scope.
+Notation "A <= B < C" := (submx A B && ltmx B C) : matrix_set_scope.
+Notation "A < B < C" := (ltmx A B && ltmx B C) : matrix_set_scope.
+Notation "A == B" := ((submx A B) && (submx B A)) : matrix_set_scope.
+Notation "A :=: B" := (eqmx A B) : matrix_set_scope.
+Notation "A + B" := (addsmx A B) : matrix_set_scope.
+Notation "A :&: B" := (capmx A B) : matrix_set_scope.
+Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
+Notation mxdirect S := (mxdirect_def (Phantom 'M_(_,_) S%MS)).
+ +
+Notation "\sum_ ( i <- r | P ) B" :=
+  (\big[addsmx/0%R]_(i <- r | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i <- r ) B" :=
+  (\big[addsmx/0%R]_(i <- r) B%MS) : matrix_set_scope.
+Notation "\sum_ ( m <= i < n | P ) B" :=
+  (\big[addsmx/0%R]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( m <= i < n ) B" :=
+  (\big[addsmx/0%R]_(m ≤ i < n) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i | P ) B" :=
+  (\big[addsmx/0%R]_(i | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ i B" :=
+  (\big[addsmx/0%R]_i B%MS) : matrix_set_scope.
+Notation "\sum_ ( i : t | P ) B" :=
+  (\big[addsmx/0%R]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
+Notation "\sum_ ( i : t ) B" :=
+  (\big[addsmx/0%R]_(i : t) B%MS) (only parsing) : matrix_set_scope.
+Notation "\sum_ ( i < n | P ) B" :=
+  (\big[addsmx/0%R]_(i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i < n ) B" :=
+  (\big[addsmx/0%R]_(i < n) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i 'in' A | P ) B" :=
+  (\big[addsmx/0%R]_(i in A | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i 'in' A ) B" :=
+  (\big[addsmx/0%R]_(i in A) B%MS) : matrix_set_scope.
+ +
+Notation "\bigcap_ ( i <- r | P ) B" :=
+  (\big[capmx/1%:M]_(i <- r | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i <- r ) B" :=
+  (\big[capmx/1%:M]_(i <- r) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( m <= i < n | P ) B" :=
+  (\big[capmx/1%:M]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( m <= i < n ) B" :=
+  (\big[capmx/1%:M]_(m ≤ i < n) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i | P ) B" :=
+  (\big[capmx/1%:M]_(i | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ i B" :=
+  (\big[capmx/1%:M]_i B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i : t | P ) B" :=
+  (\big[capmx/1%:M]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
+Notation "\bigcap_ ( i : t ) B" :=
+  (\big[capmx/1%:M]_(i : t) B%MS) (only parsing) : matrix_set_scope.
+Notation "\bigcap_ ( i < n | P ) B" :=
+  (\big[capmx/1%:M]_(i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i < n ) B" :=
+  (\big[capmx/1%:M]_(i < n) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i 'in' A | P ) B" :=
+  (\big[capmx/1%:M]_(i in A | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i 'in' A ) B" :=
+  (\big[capmx/1%:M]_(i in A) B%MS) : matrix_set_scope.

Section DirectSums.
-Variables (F : fieldType) (I : finType) (P : pred I).
+Variables (F : fieldType) (I : finType) (P : pred I).

-Lemma mxdirect_delta n f : {in P &, injective f} →
-  mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>).
+Lemma mxdirect_delta n f : {in P &, injective f} →
+  mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>).

End DirectSums.
@@ -1578,8 +1590,8 @@ Variable F : finFieldType.

-Lemma card_GL n : n > 0 →
-  #|'GL_n[F]| = (#|F| ^ 'C(n, 2) × \prod_(1 ≤ i < n.+1) (#|F| ^ i - 1))%N.
+Lemma card_GL n : n > 0 →
+  #|'GL_n[F]| = (#|F| ^ 'C(n, 2) × \prod_(1 ≤ i < n.+1) (#|F| ^ i - 1))%N.

@@ -1589,20 +1601,20 @@ row-space theory, but directly performs the LUP decomposition.
-Lemma LUP_card_GL n : n > 0 →
-  #|'GL_n[F]| = (#|F| ^ 'C(n, 2) × \prod_(1 ≤ i < n.+1) (#|F| ^ i - 1))%N.
+Lemma LUP_card_GL n : n > 0 →
+  #|'GL_n[F]| = (#|F| ^ 'C(n, 2) × \prod_(1 ≤ i < n.+1) (#|F| ^ i - 1))%N.

-Lemma card_GL_1 : #|'GL_1[F]| = #|F|.-1.
+Lemma card_GL_1 : #|'GL_1[F]| = #|F|.-1.

-Lemma card_GL_2 : #|'GL_2[F]| = (#|F| × #|F|.-1 ^ 2 × #|F|.+1)%N.
+Lemma card_GL_2 : #|'GL_2[F]| = (#|F| × #|F|.-1 ^ 2 × #|F|.+1)%N.

End CardGL.

-Lemma logn_card_GL_p n p : prime p → logn p #|'GL_n(p)| = 'C(n, 2).
+Lemma logn_card_GL_p n p : prime p → logn p #|'GL_n(p)| = 'C(n, 2).

Section MatrixAlgebra.
@@ -1613,138 +1625,138 @@

-Lemma mem0mx m n (R : 'A_(m, n)) : 0 \in R.
+Lemma mem0mx m n (R : 'A_(m, n)) : 0 \in R.

-Lemma memmx0 n A : (A \in (0 : 'A_n)) → A = 0.
+Lemma memmx0 n A : (A \in (0 : 'A_n)) → A = 0.

-Lemma memmx1 n (A : 'M_n) : (A \in mxvec 1%:M) = is_scalar_mx A.
+Lemma memmx1 n (A : 'M_n) : (A \in mxvec 1%:M) = is_scalar_mx A.

-Lemma memmx_subP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-  reflect (∀ A, A \in R1 → A \in R2) (R1 ≤ R2)%MS.
+Lemma memmx_subP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+  reflect (∀ A, A \in R1 → A \in R2) (R1 ≤ R2)%MS.

-Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-  reflect (∀ A, (A \in R1) = (A \in R2)) (R1 == R2)%MS.
+Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+  reflect (∀ A, (A \in R1) = (A \in R2)) (R1 == R2)%MS.

-Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-  reflect (∃ D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2])
-          (A \in R1 + R2)%MS.
+Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+  reflect (∃ D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2])
+          (A \in R1 + R2)%MS.

-Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ :
-  reflect (exists2 A_, A = \sum_(i | P i) A_ i & ∀ i, A_ i \in R_ i)
-          (A \in \sum_(i | P i) R_ i)%MS.
+Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ :
+  reflect (exists2 A_, A = \sum_(i | P i) A_ i & ∀ i, A_ i \in R_ i)
+          (A \in \sum_(i | P i) R_ i)%MS.

-Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) :
-    (1%:M \in R)%MS →
-  reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R).
+Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) :
+    (1%:M \in R)%MS →
+  reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R).

-Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) :=
-  (\sum_i <<R1 ×m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS.
+Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) :=
+  (\sum_i <<R1 ×m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS.



-Lemma genmx_muls m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-  <<(R1 × R2)%MS>>%MS = (R1 × R2)%MS.
+Lemma genmx_muls m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+  <<(R1 × R2)%MS>>%MS = (R1 × R2)%MS.

-Lemma mem_mulsmx m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) A1 A2 :
-  (A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R1 × R2)%MS.
+Lemma mem_mulsmx m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) A1 A2 :
+  (A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R1 × R2)%MS.

Lemma mulsmx_subP m1 m2 m n
-                 (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R : 'A_(m, n)) :
-  reflect (∀ A1 A2, A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R)
-          (R1 × R2 ≤ R)%MS.
+                 (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R : 'A_(m, n)) :
+  reflect (∀ A1 A2, A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R)
+          (R1 × R2 ≤ R)%MS.

-Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
-                            (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
-  (R1 ≤ R3 → R2 ≤ R4 → R1 × R2 ≤ R3 × R4)%MS.
+Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
+                            (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
+  (R1 ≤ R3 → R2 ≤ R4 → R1 × R2 ≤ R3 × R4)%MS.

-Lemma muls_eqmx m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
-                              (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
-  (R1 :=: R3 → R2 :=: R4 → R1 × R2 = R3 × R4)%MS.
+Lemma muls_eqmx m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
+                              (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
+  (R1 :=: R3 → R2 :=: R4 → R1 × R2 = R3 × R4)%MS.

-Lemma mulsmxP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-  reflect (exists2 A1, ∀ i, A1 i \in R1
-            & exists2 A2, ∀ i, A2 i \in R2
-           & A = \sum_(i < n ^ 2) A1 i ×m A2 i)
-          (A \in R1 × R2)%MS.
+Lemma mulsmxP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+  reflect (exists2 A1, ∀ i, A1 i \in R1
+            & exists2 A2, ∀ i, A2 i \in R2
+           & A = \sum_(i < n ^ 2) A1 i ×m A2 i)
+          (A \in R1 × R2)%MS.

-Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
-  (R1 × (R2 × R3) = R1 × R2 × R3)%MS.
+Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
+  (R1 × (R2 × R3) = R1 × R2 × R3)%MS.

Lemma mulsmx_addl m1 m2 m3 n
-                 (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
-  ((R1 + R2) × R3 = R1 × R3 + R2 × R3)%MS.
+                 (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
+  ((R1 + R2) × R3 = R1 × R3 + R2 × R3)%MS.

Lemma mulsmx_addr m1 m2 m3 n
-                  (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
-  (R1 × (R2 + R3) = R1 × R2 + R1 × R3)%MS.
+                  (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
+  (R1 × (R2 + R3) = R1 × R2 + R1 × R3)%MS.

-Lemma mulsmx0 m1 m2 n (R1 : 'A_(m1, n)) : (R1 × (0 : 'A_(m2, n)) = 0)%MS.
+Lemma mulsmx0 m1 m2 n (R1 : 'A_(m1, n)) : (R1 × (0 : 'A_(m2, n)) = 0)%MS.

-Lemma muls0mx m1 m2 n (R2 : 'A_(m2, n)) : ((0 : 'A_(m1, n)) × R2 = 0)%MS.
+Lemma muls0mx m1 m2 n (R2 : 'A_(m2, n)) : ((0 : 'A_(m1, n)) × R2 = 0)%MS.

-Definition left_mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
-  (R1 × R2 ≤ R2)%MS.
+Definition left_mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
+  (R1 × R2 ≤ R2)%MS.

-Definition right_mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
-  (R2 × R1 ≤ R2)%MS.
+Definition right_mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
+  (R2 × R1 ≤ R2)%MS.

-Definition mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
-  left_mx_ideal R1 R2 && right_mx_ideal R1 R2.
+Definition mx_ideal m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :=
+  left_mx_ideal R1 R2 && right_mx_ideal R1 R2.

-Definition mxring_id m n (R : 'A_(m, n)) e :=
-  [/\ e != 0,
-      e \in R,
-      ∀ A, A \in R → e ×m A = A
-    & ∀ A, A \in R → A ×m e = A]%MS.
+Definition mxring_id m n (R : 'A_(m, n)) e :=
+  [/\ e != 0,
+      e \in R,
+      ∀ A, A \in R → e ×m A = A
+    & ∀ A, A \in R → A ×m e = A]%MS.

-Definition has_mxring_id m n (R : 'A[F]_(m , n)) :=
-  (R != 0) &&
+Definition has_mxring_id m n (R : 'A[F]_(m , n)) :=
+  (R != 0) &&
  (row_mx 0 (row_mx (mxvec R) (mxvec R))
-    ≤ row_mx (cokermx R) (row_mx (lin_mx (mulmx R \o lin_mulmx))
-                                  (lin_mx (mulmx R \o lin_mulmxr))))%MS.
+    ≤ row_mx (cokermx R) (row_mx (lin_mx (mulmx R \o lin_mulmx))
+                                  (lin_mx (mulmx R \o lin_mulmxr))))%MS.

-Definition mxring m n (R : 'A_(m, n)) :=
-  left_mx_ideal R R && has_mxring_id R.
+Definition mxring m n (R : 'A_(m, n)) :=
+  left_mx_ideal R R && has_mxring_id R.

-Lemma mxring_idP m n (R : 'A_(m, n)) :
-  reflect (∃ e, mxring_id R e) (has_mxring_id R).
+Lemma mxring_idP m n (R : 'A_(m, n)) :
+  reflect (∃ e, mxring_id R e) (has_mxring_id R).

Section CentMxDef.

-Variables (m n : nat) (R : 'A[F]_(m, n)).
+Variables (m n : nat) (R : 'A[F]_(m, n)).

-Definition cent_mx_fun (B : 'M[F]_n) := R ×m lin_mx (mulmxr B \- mulmx B).
+Definition cent_mx_fun (B : 'M[F]_n) := R ×m lin_mx (mulmxr B \- mulmx B).

Lemma cent_mx_fun_is_linear : linear cent_mx_fun.
@@ -1755,7 +1767,7 @@ Definition cent_mx := kermx (lin_mx cent_mx_fun).

-Definition center_mx := (R :&: cent_mx)%MS.
+Definition center_mx := (R :&: cent_mx)%MS.

End CentMxDef.
@@ -1763,45 +1775,45 @@

-Lemma cent_rowP m n B (R : 'A_(m, n)) :
-  reflect (∀ i (A := vec_mx (row i R)), A ×m B = B ×m A) (B \in 'C(R))%MS.
+Lemma cent_rowP m n B (R : 'A_(m, n)) :
+  reflect (∀ i (A := vec_mx (row i R)), A ×m B = B ×m A) (B \in 'C(R))%MS.

-Lemma cent_mxP m n B (R : 'A_(m, n)) :
-  reflect (∀ A, A \in R → A ×m B = B ×m A) (B \in 'C(R))%MS.
+Lemma cent_mxP m n B (R : 'A_(m, n)) :
+  reflect (∀ A, A \in R → A ×m B = B ×m A) (B \in 'C(R))%MS.

-Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS.
+Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS.

-Lemma center_mx_sub m n (R : 'A_(m, n)) : ('Z(R) ≤ R)%MS.
+Lemma center_mx_sub m n (R : 'A_(m, n)) : ('Z(R) ≤ R)%MS.

-Lemma center_mxP m n A (R : 'A_(m, n)) :
-  reflect (A \in R ∧ ∀ B, B \in R → B ×m A = A ×m B)
-          (A \in 'Z(R))%MS.
+Lemma center_mxP m n A (R : 'A_(m, n)) :
+  reflect (A \in R ∧ ∀ B, B \in R → B ×m A = A ×m B)
+          (A \in 'Z(R))%MS.

-Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 :
-  mxring_id R e1 → mxring_id R e2 → e1 = e2.
+Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 :
+  mxring_id R e1 → mxring_id R e2 → e1 = e2.

-Lemma cent_mx_ideal m n (R : 'A_(m, n)) : left_mx_ideal 'C(R)%MS 'C(R)%MS.
+Lemma cent_mx_ideal m n (R : 'A_(m, n)) : left_mx_ideal 'C(R)%MS 'C(R)%MS.

-Lemma cent_mx_ring m n (R : 'A_(m, n)) : n > 0 → mxring 'C(R)%MS.
+Lemma cent_mx_ring m n (R : 'A_(m, n)) : n > 0 → mxring 'C(R)%MS.

-Lemma mxdirect_adds_center m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
-    mx_ideal (R1 + R2)%MS R1 → mx_ideal (R1 + R2)%MS R2 →
-    mxdirect (R1 + R2) →
-  ('Z((R1 + R2)%MS) :=: 'Z(R1) + 'Z(R2))%MS.
+Lemma mxdirect_adds_center m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
+    mx_ideal (R1 + R2)%MS R1 → mx_ideal (R1 + R2)%MS R2 →
+    mxdirect (R1 + R2) →
+  ('Z((R1 + R2)%MS) :=: 'Z(R1) + 'Z(R2))%MS.

-Lemma mxdirect_sums_center (I : finType) m n (R : 'A_(m, n)) R_ :
-    (\sum_i R_ i :=: R)%MS → mxdirect (\sum_i R_ i) →
-    (∀ i : I, mx_ideal R (R_ i)) →
-  ('Z(R) :=: \sum_i 'Z(R_ i))%MS.
+Lemma mxdirect_sums_center (I : finType) m n (R : 'A_(m, n)) R_ :
+    (\sum_i R_ i :=: R)%MS → mxdirect (\sum_i R_ i) →
+    (∀ i : I, mx_ideal R (R_ i)) →
+  ('Z(R) :=: \sum_i 'Z(R_ i))%MS.

End MatrixAlgebra.
@@ -1809,14 +1821,12 @@

- -
-Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope.
-Notation "R * S" := (mulsmx R S) : matrix_set_scope.
-Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope.
-Notation "''C_' R ( S )" := (R :&: 'C(S))%MS : matrix_set_scope.
-Notation "''C_' ( R ) ( S )" := ('C_R(S))%MS (only parsing) : matrix_set_scope.
-Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.
+Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope.
+Notation "R * S" := (mulsmx R S) : matrix_set_scope.
+Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope.
+Notation "''C_' R ( S )" := (R :&: 'C(S))%MS : matrix_set_scope.
+Notation "''C_' ( R ) ( S )" := ('C_R(S))%MS (only parsing) : matrix_set_scope.
+Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.

@@ -1830,101 +1840,99 @@ Section MapMatrixSpaces.

-Variables (aF rF : fieldType) (f : {rmorphism aF → rF}).
+Variables (aF rF : fieldType) (f : {rmorphism aF → rF}).

-Lemma Gaussian_elimination_map m n (A : 'M_(m, n)) :
-  Gaussian_elimination A^f = ((col_ebase A)^f, (row_ebase A)^f, \rank A).
+Lemma Gaussian_elimination_map m n (A : 'M_(m, n)) :
+  Gaussian_elimination A^f = ((col_ebase A)^f, (row_ebase A)^f, \rank A).

-Lemma mxrank_map m n (A : 'M_(m, n)) : \rank A^f = \rank A.
+Lemma mxrank_map m n (A : 'M_(m, n)) : \rank A^f = \rank A.

-Lemma row_free_map m n (A : 'M_(m, n)) : row_free A^f = row_free A.
+Lemma row_free_map m n (A : 'M_(m, n)) : row_free A^f = row_free A.

-Lemma row_full_map m n (A : 'M_(m, n)) : row_full A^f = row_full A.
+Lemma row_full_map m n (A : 'M_(m, n)) : row_full A^f = row_full A.

-Lemma map_row_ebase m n (A : 'M_(m, n)) : (row_ebase A)^f = row_ebase A^f.
+Lemma map_row_ebase m n (A : 'M_(m, n)) : (row_ebase A)^f = row_ebase A^f.

-Lemma map_col_ebase m n (A : 'M_(m, n)) : (col_ebase A)^f = col_ebase A^f.
+Lemma map_col_ebase m n (A : 'M_(m, n)) : (col_ebase A)^f = col_ebase A^f.

-Lemma map_row_base m n (A : 'M_(m, n)) :
-  (row_base A)^f = castmx (mxrank_map A, erefl n) (row_base A^f).
+Lemma map_row_base m n (A : 'M_(m, n)) :
+  (row_base A)^f = castmx (mxrank_map A, erefl n) (row_base A^f).

-Lemma map_col_base m n (A : 'M_(m, n)) :
-  (col_base A)^f = castmx (erefl m, mxrank_map A) (col_base A^f).
+Lemma map_col_base m n (A : 'M_(m, n)) :
+  (col_base A)^f = castmx (erefl m, mxrank_map A) (col_base A^f).

-Lemma map_pinvmx m n (A : 'M_(m, n)) : (pinvmx A)^f = pinvmx A^f.
+Lemma map_pinvmx m n (A : 'M_(m, n)) : (pinvmx A)^f = pinvmx A^f.

-Lemma map_kermx m n (A : 'M_(m, n)) : (kermx A)^f = kermx A^f.
+Lemma map_kermx m n (A : 'M_(m, n)) : (kermx A)^f = kermx A^f.

-Lemma map_cokermx m n (A : 'M_(m, n)) : (cokermx A)^f = cokermx A^f.
+Lemma map_cokermx m n (A : 'M_(m, n)) : (cokermx A)^f = cokermx A^f.

-Lemma map_submx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A^f ≤ B^f)%MS = (A ≤ B)%MS.
+Lemma map_submx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A^f ≤ B^f)%MS = (A ≤ B)%MS.

-Lemma map_ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A^f < B^f)%MS = (A < B)%MS.
+Lemma map_ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A^f < B^f)%MS = (A < B)%MS.

-Lemma map_eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (A^f :=: B^f)%MS ↔ (A :=: B)%MS.
+Lemma map_eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A^f :=: B^f)%MS ↔ (A :=: B)%MS.

-Lemma map_genmx m n (A : 'M_(m, n)) : (<<A>>^f :=: <<A^f>>)%MS.
+Lemma map_genmx m n (A : 'M_(m, n)) : (<<A>>^f :=: <<A^f>>)%MS.

-Lemma map_addsmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (((A + B)%MS)^f :=: A^f + B^f)%MS.
+Lemma map_addsmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (((A + B)%MS)^f :=: A^f + B^f)%MS.

-Lemma map_capmx_gen m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  (capmx_gen A B)^f = capmx_gen A^f B^f.
+Lemma map_capmx_gen m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (capmx_gen A B)^f = capmx_gen A^f B^f.

-Lemma map_capmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  ((A :&: B)^f :=: A^f :&: B^f)%MS.
+Lemma map_capmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  ((A :&: B)^f :=: A^f :&: B^f)%MS.

-Lemma map_complmx m n (A : 'M_(m, n)) : (A^C^f = A^f^C)%MS.
+Lemma map_complmx m n (A : 'M_(m, n)) : (A^C^f = A^f^C)%MS.

-Lemma map_diffmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
-  ((A :\: B)^f :=: A^f :\: B^f)%MS.
+Lemma map_diffmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  ((A :\: B)^f :=: A^f :\: B^f)%MS.

-Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a)^f = eigenspace g^f (f a).
+Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a)^f = eigenspace g^f (f a).

-Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g^f (f a) = eigenvalue g a.
+Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g^f (f a) = eigenvalue g a.

-Lemma memmx_map m n A (E : 'A_(m, n)) : (A^f \in E^f)%MS = (A \in E)%MS.
+Lemma memmx_map m n A (E : 'A_(m, n)) : (A^f \in E^f)%MS = (A \in E)%MS.

-Lemma map_mulsmx m1 m2 n (E1 : 'A_(m1, n)) (E2 : 'A_(m2, n)) :
-  ((E1 × E2)%MS^f :=: E1^f × E2^f)%MS.
+Lemma map_mulsmx m1 m2 n (E1 : 'A_(m1, n)) (E2 : 'A_(m2, n)) :
+  ((E1 × E2)%MS^f :=: E1^f × E2^f)%MS.

-Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS.
+Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS.

-Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS.
+Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS.

End MapMatrixSpaces.
- -
-- cgit v1.2.3