Library mxalgebra

 In this file we develop the rank and row space theory of matrices, based  
 on an extended gaussian elimination procedure similar to LUP              
 decomposition. This provides us with a concrete but generic model of      
 finite dimensional vector spaces and F-algebras, in which vectors, linear 
 functions, families, bases, subspaces, ideals and subrings are all        
 represented using matrices. This model can be used as a foundation for    
 the usual theory of abstract linear algebra, but it can also be used to   
 develop directly substantial theories, such as the theory of finite group 
 linear representation.                                                    
   Here we define the following concepts and notations:                    
 gaussian_elimination A == a permuted triangular decomposition (L, U, r)   
                   of A, with L a column permutation of a lower triangular 
                   invertible matrix, U a row permutation of an upper      
                   triangular invertible matrix, and r the rank of A, all  
                   satisfying the identity L *m pid_mx r *m U = A.         
        \rank A == the rank of A.                                          
    row_free A <=> the rows of A are linearly free (i.e., the rank and     
                   height of A are equal).                                 
    row_full A <=> the row-space of A spans all row-vectors (i.e., the     
                   rank and width of A are equal).                         
    col_ebase A == the extended column basis of A (the first matrix L      
                   returned by gaussian_elimination A).                    
    row_ebase A == the extended row base of A (the second matrix U         
                   returned by gaussian_elimination A).                    
     col_base A == a basis for the columns of A: a row-full matrix         
                   consisting of the first \rank A columns of col_ebase A. 
     row_base A == a basis for the rows of A: a row-free matrix consisting 
                   of the first \rank A rows of row_ebase A.               
       pinvmx A == a partial inverse for A in its row space (or on its     
                   column space, equivalently). In particular, if u is a   
                   row vector in the row_space of A, then u *m pinvmx A is 
                   the row vector of the coefficients of a decomposition   
                   of u as a sub of rows of A.                             
        kermx A == the row kernel of A : a square matrix whose row space   
                   consists of all u such that u *m A = 0 (it consists of  
                   the inverse of col_ebase A, with the top \rank A rows   
                   zeroed out). Also, kermx A is a partial right inverse   
                   to col_ebase A, in the row space anihilated by A.       
      cokermx A == the cokernel of A : a square matrix whose column space  
                   consists of all v such that A *m v = 0 (it consists of  
                   the inverse of row_ebase A, with the leftmost \rank A   
                   columns zeroed out).                                    
 eigenvalue g a <=> a is an eigenvalue of the square matrix g.             
 eigenspace g a == a square matrix whose row space is the eigenspace of    
                   the eigenvalue a of g (or 0 if a is not an eigenvalue). 
 We use a different scope %MS for matrix row-space set-like operations; to 
 avoid confusion, this scope should not be opened globally. Note that the  
 the arguments of \rank _ and the operations below have default scope %MS. 
    (A <= B)%MS <=> the row-space of A is included in the row-space of B.  
                   We test for this by testing if cokermx B anihilates A.  
     (A < B)%MS <=> the row-space of A is properly included in the         
                   row-space of B.                                         
  (A <= B <= C)%MS == (A <= B)%MS && (B <= C)%MS, and similarly for        
                   (A < B <= C)%MS, (A < B <= C)%MS and (A < B < C)%MS.    
    (A == B)%MS == (A <= B <= A)%MS (A and B have the same row-space).     
   (A :=: B)%MS == A and B behave identically wrt. \rank and <=. This      
                   triple rewrite rule is the Prop version of (A == B)%MS. 
                   Note that :=: cannot be treated as a setoid-style       
                   Equivalence because its arguments can have different    
                   types: A and B need not have the same number of rows,   
                   and often don't (e.g., in row_base A :=: A).            
       <<A>>%MS == a square matrix with the same row-space as A; <<A>>%MS  
                   is a canonical representation of the subspace generated 
                   by A, viewed as a list of row-vectors: if (A == B)%MS,  
                   then <<A>>%MS = <<B>>%MS.                               
     (A + B)%MS == a square matrix whose row-space is the sum of the       
                   row-spaces of A and B; thus (A + B == col_mx A B)%MS.   
  (\sum_i <expr i>)%MS == the "big" version of (_ + _)%MS; as the latter   
                   has a canonical abelian monoid structure, most generic  
                   bigop lemmas apply (the other bigop indexing notations  
                   are also defined).                                      
   (A :&: B)%MS == a square matrix whose row-space is the intersection of  
                   the row-spaces of A and B.                              
  (\bigcap_i <expr i>)%MS == the "big" version of (_ :&: _)%MS, which also 
                   has a canonical abelian monoid structure.               
         A^C%MS == a square matrix whose row-space is a complement to the  
                   the row-space of A (it consists of row_ebase A with the 
                   top \rank A rows zeroed out).                           
   (A :\: B)%MS == a square matrix whose row-space is a complement of the  
                   the row-space of (A :&: B)%MS in the row-space of A.    
                   We have (A :\: B == A :&: (capmx_gen A B)^C)%MS, with   
                   capmx_gen A B a recatangular matrix that generates      
                   (A :&: B)%MS, i.e., (capmx_gen A B == A :&: B)%MS.      
    proj_mx A B == a square matrix that projects (A + B)%MS onto A         
                   parellel to B, when (A :&: B)%MS = 0 (A and B must also 
                   be square).                                             
     mxdirect S == the sum expression S is a direct sum. This is a NON     
                   EXTENSIONAL notation: the exact boolean expression is   
                   inferred from the syntactic form of S (expanding        
                   definitions, however); both (\sum_(i | _) _)%MS and     
                   (_ + _)%MS sums are recognized. This construct uses a   
                   variant of the reflexive ("quote") canonical structure, 
                   mxsum_expr. The structure also recognizes sums of       
                   matrix ranks, so that lemmas concerning the rank of     
                   direct sums can be used bidirectionally.                
 The next set of definitions let us represent F-algebras using matrices:   
   'A[F]_(m, n) == the type of matrices encoding (sub)algebras of square   
                   n x n matrices, via mxvec; as in the matrix type        
                   notation, m and F can be omitted (m defaults to n ^ 2). 
                := 'M[F]_(m, n ^ 2).                                       
   (A \in R)%MS <=> the square matrix A belongs to the linear set of       
                    matrices (most often, a sub-algebra) encoded by the    
                    row space of R. This is simply notation, so all the    
                    lemmas and rewrite rules for (_ <= _)%MS can apply.    
                := (mxvec A <= R)%MS.                                      
     (R * S)%MS == a square n^2 x n^2 matrix whose row-space encodes the   
                   linear set of n x n matrices generated by the pointwise 
                   product of the sets of matrices encoded by R and S.     
       'C(R)%MS == a square matric encoding the centraliser of the set of  
                   square matrices encoded by R.                           
     'C_S(R)%MS := (S :&: 'C(R))%MS (the centraliser of R in S).           
       'Z(R)%MS == the center of R (i.e., 'C_R(R)%MS).                     
  left_mx_ideal R S <=> S is a left ideal for R (R * S <= S)%MS.           
 right_mx_ideal R S <=> S is a right ideal for R (S * R <= S)%MS.          
       mx_ideal R S <=> S is a bilateral ideal for R.                      
      mxring_id R e <-> e is an identity element for R (Prop predicate).   
    has_mxring_id R <=> R has a nonzero identity element (bool predicate). 
           mxring R <=> R encodes a nontrivial subring.                    


Import GroupScope.
Import GRing.Theory.
Open Local Scope ring_scope.

Reserved Notation "\rank A" (at level 10, A at level 8, format "\rank A").
Reserved Notation "A :+: B" (at level 50, left associativity).
Reserved Notation "A ^C" (at level 8, format "A ^C").

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

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

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)
  (at level 8, only parsing) : type_scope.

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

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

Delimit Scope matrix_set_scope with MS.

Notation Local simp := (Monoid.Theory.simpm, oppr0).

 Rank and row-space theory 

Section RowSpaceTheory.

Variable F : fieldType.

Local Notation "''M_' ( m , n )" := 'M[F]_(m, n) : type_scope.
Local Notation "''M_' n" := 'M[F]_(n, n) : type_scope.

 Decomposition with double pivoting; computes the rank, row and column  
 images, kernels, and complements of a matrix.                          

Fixpoint gaussian_elimination {m n} : 'M_(m, n) -> 'M_m * 'M_n * nat :=
  match m, n return 'M_(m, n) -> 'M_m * 'M_n * nat with
  | _.+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)
  end.

Section Defs.

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


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_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 pinvmx : 'M_(n, m) :=
  invmx row_ebase *m pid_mx mxrank *m invmx col_ebase.

End Defs.

Local Notation "\rank A" := (mxrank A) : nat_scope.
Local Notation "A ^C" := (complmx A) : matrix_set_scope.

Let mxopE : forall k opty (op : forall m : nat, opty m) m1,
  (let f := let: tt := k in fun m => op m in f) m1 = op m1.

Definition submx_def m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
  A *m cokermx B == 0.
Fact submx_key : unit.
Definition submx := let: tt := submx_key in submx_def.
Local Notation "A <= B" := (submx A B) : matrix_set_scope.
Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope.
Local Notation "A == B" := (A <= B <= A)%MS : matrix_set_scope.

Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
  (A <= B)%MS && ~~ (B <= A)%MS.
Local Notation "A < B" := (ltmx A B) : matrix_set_scope.

Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
  prod (\rank A = \rank B)
       (forall m3 (C : 'M_(m3, n)),
            ((A <= C) = (B <= C)) * ((C <= A) = (C <= B)))%MS.
Local Notation "A :=: B" := (eqmx A B) : matrix_set_scope.

Section LtmxIdentities.

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 ltmxW : (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.

End LtmxIdentities.

 The definition of the row-space operator is rigged to return the identity  
 matrix for full matrices. To allow for further tweaks that will make the   
 row-space intersection operator strictly commutative and monoidal, we      
 slightly generalize some auxiliary definitions: we parametrize the         
 "equivalent subspace and identity" choice predicate equivmx by a boolean   
 determining whether the matrix should be the identity (so for genmx A its  
 value is row_full A), and introduce a "quasi-identity" predicate qidmx     
 that selects non-square full matrices along with the identity matrix 1%:M  
 (this does not affect genmx, which chooses a square matrix).               
   The choice witness for genmx A is either 1%:M for a row-full A, or else  
 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 m n (A : 'M_(m, n)) : 'M_n :=
  choose (equivmx A (row_full A)) (genmx_witness A).
Fact genmx_key : unit.
Definition genmx := let: tt := genmx_key in genmx_def.
Local Notation "<< A >>" := (genmx A) : matrix_set_scope.

 The setwise sum is tweaked so that 0 is a strict identity element for      
 square matrices, because this lets us use the bigop component. As a result 
 setwise sum is not quite strictly extensional.                             
Let addsmx_nop m n (A : 'M_(m, n)) := conform_mx <<A>>%MS A.
Definition addsmx_def m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : 'M_n :=
  if A == 0 then addsmx_nop B else if B == 0 then addsmx_nop A else
  <<col_mx A B>>%MS.
Fact addsmx_key : unit.
Definition addsmx := let: tt := addsmx_key in addsmx_def.
Local Notation "A + B" := (addsmx A B) : matrix_set_scope.
Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS)
  : matrix_set_scope.

 The set intersection is similarly biased so that the identity matrix is a  
 strict identity. This is somewhat more delicate than for the sum, because  
 the test for the identity is non-extensional. This forces us to actually   
 bias the choice operator so that it does not accidentally map an           
 intersection of non-identity matrices to 1%:M; this would spoil            
 associativity: if B :&: C = 1%:M but B and C are not identity, then for a  
 square matrix A we have A :&: (B :&: C) = A != (A :&: B) :&: C in general. 
 To complicate matters there may not be a square non-singular matrix        
 different than 1%:M, since we could be dealing with 'M['F_2]_1. We         
 sidestep the issue by making all non-square row-full matrices identities,  
 and choosing a normal representative that preserves the qidmx property.    
 Thus A :&: B = 1%:M iff A and B are both identities, and this suffices for 
 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)) :=
  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 m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : 'M_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).
Fact capmx_key : unit.
Definition capmx := let: tt := capmx_key in capmx_def.
Local Notation "A :&: B" := (capmx A B) : matrix_set_scope.
Local Notation "\bigcap_ ( i | P ) B" := (\big[capmx/1%:M]_(i | P) B)
  : matrix_set_scope.

Definition diffmx_def m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : 'M_n :=
  <<capmx_gen A (capmx_gen A B)^C>>%MS.
Fact diffmx_key : unit.
Definition diffmx := let: tt := diffmx_key in diffmx_def.
Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope.

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

Local Notation gaussE := gaussian_elimination.

Fact mxrankE : forall m n (A : 'M_(m, n)), \rank A = (gaussE A).2.

Lemma rank_leq_row : forall m n (A : 'M_(m, n)), \rank A <= m.

Lemma row_leq_rank : forall m n (A : 'M_(m, n)), (m <= \rank A) = row_free A.

Lemma rank_leq_col : forall m n (A : 'M_(m, n)), \rank A <= n.

Lemma col_leq_rank : forall m n (A : 'M_(m, n)), (n <= \rank A) = row_full A.

Lemma row_ebase_unit : forall m n (A : 'M_(m, n)), row_ebase A \in unitmx.

Lemma col_ebase_unit : forall 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 mulmx_ebase : forall m n (A : 'M_(m, n)),
  col_ebase A *m pid_mx (\rank A) *m row_ebase A = A.

Lemma mulmx_base : forall m n (A : 'M_(m, n)), col_base A *m row_base A = A.

Lemma mulmx1_min_rank : forall r m n (A : 'M_(m, n)) M N,
  M *m A *m N = 1%:M :> 'M_r -> r <= \rank A.
Implicit Arguments mulmx1_min_rank [r m n A].

Lemma mulmx_max_rank : forall r m n (M : 'M_(m, r)) (N : 'M_(r, n)),
  \rank (M *m N) <= r.
Implicit Arguments mulmx_max_rank [r m n].

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

Lemma mxrank_add : forall m n (A B : 'M_(m, n)),
  \rank (A + B)%R <= \rank A + \rank B.

Lemma mxrankM_maxl : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  \rank (A *m B) <= \rank A.

Lemma mxrankM_maxr : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  \rank (A *m B) <= \rank B.

Lemma mxrank_scale : forall m n a (A : 'M_(m, n)),
  \rank (a *: A) <= \rank A.

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

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

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

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

Lemma mulmx_coker : forall m n (A : 'M_(m, n)), A *m cokermx A = 0.

Lemma submxE : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A <= B)%MS = (A *m cokermx B == 0).

Lemma mulmxKpV : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A <= B)%MS -> A *m pinvmx B *m B = A.

Lemma submxP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (exists D, A = D *m B) (A <= B)%MS.
Implicit Arguments submxP [m1 m2 n A B].

Lemma submx_refl : forall m n (A : 'M_(m, n)), (A <= A)%MS.
Hint Resolve submx_refl.

Lemma submxMl : forall m n p (D : 'M_(m, n)) (A : 'M_(n, p)),
  (D *m A <= A)%MS.

Lemma submxMr : forall m1 m2 n p,
                   forall (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 : forall m n1 n2 p (C : 'M_(m, n1)) A (B : 'M_(n2, p)),
  (A <= B -> C *m A <= B)%MS.

Lemma submx_trans : forall m1 m2 m3 n,
    forall (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)),
  (A <= B -> B <= C -> A <= C)%MS.

Lemma ltmx_sub_trans : forall 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 sub_ltmx_trans : forall 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 ltmx_trans : forall m n, transitive (@ltmx m m n).

Lemma ltmx_irrefl : forall m n, irreflexive (@ltmx m m n).

Lemma sub0mx : forall m1 m2 n (A : 'M_(m2, n)),
  ((0 : 'M_(m1, n)) <= A)%MS.

Lemma submx0null : forall m1 m2 n (A : 'M[F]_(m1, n)),
  (A <= (0 : 'M_(m2, n)))%MS -> A = 0.

Lemma submx0 : forall m n (A : 'M_(m, n)), (A <= (0 : 'M_n))%MS = (A == 0).

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

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

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

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

Lemma addmx_sub : forall m1 m2 n,
                  forall (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 : forall m1 m2 n (B : 'M_(m2, n)),
                     forall I r (P : pred I) (A_ : I -> 'M_(m1, n)),
  (forall i, P i -> A_ i <= B)%MS -> ((\sum_(i <- r | P i) A_ i)%R <= B)%MS.

Lemma scalemx_sub : forall m1 m2 n a (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A <= B)%MS -> (a *: A <= B)%MS.

Lemma row_sub : forall m n i (A : 'M_(m, n)), (row i A <= A)%MS.

Lemma eq_row_sub : forall m n v (A : 'M_(m, n)) i, row i A = v -> (v <= A)%MS.

Lemma nz_row_sub : forall m n (A : 'M_(m, n)), (nz_row A <= A)%MS.

Lemma row_subP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (forall i, row i A <= B)%MS (A <= B)%MS.
Implicit Arguments row_subP [m1 m2 n A B].

Lemma rV_subP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (forall v : 'rV_n, v <= A -> v <= B)%MS (A <= B)%MS.
Implicit Arguments rV_subP [m1 m2 n A B].

Lemma row_subPn : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS).

Lemma sub_rVP : forall n (u v : 'rV_n),
  reflect (exists a, u = a *: v) (u <= v)%MS.

Lemma rank_rV : forall n (v : 'rV_n), \rank v = (v != 0).

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

Lemma rowV0P : forall m n (A : 'M_(m, n)),
  reflect (forall v : 'rV_n, v <= A -> v = 0)%MS (A == 0).

Lemma submx_full : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  row_full B -> (A <= B)%MS.

Lemma row_fullP : forall m n (A : 'M_(m, n)),
  reflect (exists B, B *m A = 1%:M) (row_full A).
Implicit Arguments row_fullP [m n A].

Lemma row_full_inj : forall m n p A, row_full A -> injective (@mulmx _ m n p A).

Lemma row_freeP : forall m n (A : 'M_(m, n)),
  reflect (exists B, A *m B = 1%:M) (row_free A).

Lemma row_free_inj : forall m n p A,
  row_free A -> injective ((@mulmx _ m n p)^~ A).

Lemma row_free_unit : forall n (A : 'M_n), row_free A = (A \in unitmx).

Lemma row_full_unit : forall n (A : 'M_n), row_full A = (A \in unitmx).

Lemma mxrank_unit : forall n (A : 'M_n), A \in unitmx -> \rank A = n.

Lemma mxrank1 : forall n, \rank (1%:M : 'M_n) = n.

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

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

Lemma submx1 : forall m n (A : 'M_(m, n)), (A <= 1%:M)%MS.

Lemma sub1mx : forall m n (A : 'M_(m, n)), (1%:M <= A)%MS = row_full A.

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

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

Lemma eqmxP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (A :=: B)%MS (A == B)%MS.
Implicit Arguments eqmxP [m1 m2 n A B].

Lemma rV_eqP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (forall u : 'rV_n, (u <= A) = (u <= B))%MS (A == B)%MS.

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

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

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

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

Lemma lt_eqmx : forall m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
    (A :=: B)%MS ->
  forall C : 'M_(m3, n), (((A < C) = (B < C))%MS * ((C < A) = (C < B))%MS)%type.

Lemma eqmxMr : forall m1 m2 n p,
               forall (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(n, p)),
  (A :=: B)%MS -> (A *m C :=: B *m C)%MS.

Lemma eqmxMfull : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  row_full A -> (A *m B :=: B)%MS.

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

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

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

Lemma submxMfree : forall m1 m2 n p,
                     forall (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 : forall m1 m2 n p,
               forall (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 : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  row_free B -> \rank (A *m B) = \rank A.

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

Let qidmx_eq1 : forall n (A : 'M_n), qidmx A = (A == 1%:M).

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

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

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

Lemma genmxP : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (<<A>> = <<B>>)%MS (A == B)%MS.
Implicit Arguments genmxP [m1 m2 n A B].

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

Lemma genmx1 : forall n, <<1%:M : 'M_n>>%MS = 1%:M.

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

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

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

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

Lemma mxrank_leqif_sup : forall 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 : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A <= B)%MS -> \rank A <= \rank B ?= iff (A == B)%MS.

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

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

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

Lemma eqmx_conform : forall 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 : forall 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)).

Lemma col_mx_sub : forall 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 addsmx_sub : forall m3 (C : 'M_(m3, n)),
  (A + B <= C)%MS = (A <= C)%MS && (B <= C)%MS.

Lemma addsmxSl : (A <= A + B)%MS.

Lemma addsmxSr : (B <= 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.

End AddsmxSub.

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

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

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

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

Let addsmx_nop_id : forall n (A : 'M_n), addsmx_nop A = A.

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

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

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

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

Canonical Structure addsmx_monoid n :=
  Monoid.Law (@addsmxA n n n n) (@adds0mx_id n n) (@addsmx0_id n n).
Canonical Structure addsmx_comoid n := Monoid.ComLaw (@addsmxC n n n).

Lemma addsmxMr : forall m1 m2 n p,
                forall (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 : forall m1 m2 m3 m4 n,
    forall (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 : forall m m1 m2 n,
    forall (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 : forall 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 : forall 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 : forall m1 m2 m3 m4 n,
    forall (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 : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (<<(A + B)%MS>> = <<A>> + <<B>>)%MS.

Lemma sub_addsmxP : forall m1 m2 m3 n,
                  forall (A : 'M[F]_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)),
  reflect (exists u, A = u.1 *m B + u.2 *m C) (A <= B + C)%MS.
Implicit Arguments sub_addsmxP [m1 m2 m3 n A B C].

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

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

Lemma sumsmx_sup : forall 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.
Implicit Arguments sumsmx_sup [P m n A B_].

Lemma sumsmx_subP : forall P m n (A_ : I -> 'M_n) (B : 'M_(m, n)),
  reflect (forall i, P i -> A_ i <= B)%MS (\sum_(i | P i) A_ i <= B)%MS.

Lemma summx_sub_sums : forall P m n (A : I -> 'M[F]_(m, n)) B,
    (forall i, P i -> A i <= B i)%MS ->
  ((\sum_(i | P i) A i)%R <= \sum_(i | P i) B i)%MS.

Lemma sumsmxS : forall P n (A B : I -> 'M[F]_n),
    (forall i, P i -> A i <= B i)%MS ->
  (\sum_(i | P i) A i <= \sum_(i | P i) B i)%MS.

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

Lemma sub_sumsmxP : forall P m n (A : 'M_(m, n)) (B_ : I -> 'M_n),
  reflect (exists u_, A = \sum_(i | P i) u_ i *m B_ i)
          (A <= \sum_(i | P i) B_ i)%MS.

Lemma sumsmxMr_gen : forall 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 : forall 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 : forall m n r,
  r <= m -> r <= n -> \rank (pid_mx r : 'M_(m, n)) = r.

Lemma rank_copid_mx : forall n r,
  r <= n -> \rank (copid_mx r : 'M_n) = (n - r)%N.

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

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

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

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

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

Lemma mulmx_ker : forall m n (A : 'M_(m, n)), kermx A *m A = 0.

Lemma mulmxKV_ker : forall 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 : forall p m n (A : 'M_(m, n)) (B : 'M_(p, m)),
  reflect (B *m A = 0) (B <= kermx A)%MS.

Lemma det0P : forall n (A : 'M_n),
  reflect (exists2 v : 'rV[F]_n, v != 0 & v *m A = 0) (\det A == 0).

Lemma mulmx0_rank_max : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  A *m B = 0 -> \rank A + \rank B <= n.

Lemma mxrank_Frobenius : forall 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 : forall m n p (A : 'M_(m, n)) (B : 'M_(n, p)),
  \rank A + \rank B - n <= \rank (A *m B).

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

Lemma sub_capmx_gen : forall m1 m2 m3 n,
    forall (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 : forall m n (A : 'M_(m, n)),
  equivmx A (qidmx A) (capmx_witness A).

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

Let capmx_norm_eq : forall 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 : forall m n (A : 'M_(m, n)),
  equivmx_spec A (qidmx A) (capmx_nop A).

Let sub_qidmx : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  qidmx B -> (A <= B)%MS.

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

Let capmx_eq_norm : forall 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 : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :&: B :=: capmx_gen A B)%MS.

Lemma capmxSl : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :&: B <= A)%MS.

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

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

Lemma capmxSr : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :&: B <= B)%MS.

Lemma capmx_idPr : forall n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (A :&: B :=: B)%MS (B <= A)%MS.

Lemma capmx_idPl : forall n m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  reflect (A :&: B :=: A)%MS (A <= B)%MS.

Lemma capmxS : forall m1 m2 m3 m4 n,
    forall (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 : forall m1 m2 m3 m4 n,
    forall (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 : forall m1 m2 n p,
    forall (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 : forall m1 m2 n (A : 'M_(m2, n)), ((0 : 'M_(m1, n)) :&: A)%MS = 0.

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

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

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

Let capmx_nop_id : forall n (A : 'M_n), capmx_nop A = A.

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

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

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

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

Canonical Structure capmx_monoid n :=
  Monoid.Law (@capmxA n n n n) (@cap1mx n) (@capmx1 n).
Canonical Structure capmx_comoid n := Monoid.ComLaw (@capmxC n n n).

Lemma bigcapmx_inf : forall 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 : forall P m n (A : 'M_(m, n)) (B_ : I -> 'M_n),
  reflect (forall i, P i -> A <= B_ i)%MS (A <= \bigcap_(i | P i) B_ i)%MS.

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

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

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

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

Lemma mxrank_mul_ker : forall 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 : forall 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 : forall 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 : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :\: B :=: A :&: (capmx_gen A B)^C)%MS.

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

Lemma diffmxSl : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A :\: B <= A)%MS.

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

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

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

Lemma mxrank_sum_cap : forall 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 : forall 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.

 Subspace projection matrix 

Lemma proj_mx_sub : forall m n U V (W : 'M_(m, n)), (W *m proj_mx U V <= U)%MS.

Lemma proj_mx_compl_sub : forall m n U V (W : 'M_(m, n)),
  (W <= U + V -> W - W *m proj_mx U V <= V)%MS.

Lemma proj_mx_id : forall 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 : forall 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 : forall 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.
 2min: 
 rewrite !{1}addmx_sub ?proj_mx_sub ?eqmx_opp ?proj_mx_compl_sub //. 
 1s:   

Lemma proj_mx_proj : forall n (U V : 'M_n),
  (U :&: V = 0)%MS -> let P := proj_mx U V in P *m P = P.

 Completing a partially injective matrix to get a unit matrix. 

Lemma complete_unitmx : forall 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}.

 Mapping between two subspaces with the same dimension. 

Lemma eq_rank_unitmx : forall 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.

 This is the infrastructure to support the mxdirect predicate. We use a     
 bespoke canonical structure to decompose a matrix expression into binary   
 and n-ary products, using some of the "quote" technology. This lets us     
 characterize direct sums as set sums whose rank is equal to the sum of the 
 ranks of the individual terms. The mxsum_expr/proper_mxsum_expr structures 
 below supply both the decomposition and the calculation of the rank sum.   
 The mxsum_spec dependent predicate family expresses the consistency of     
 these two decompositions.                                                  
   The main technical difficulty we need to overcome is the fact that       
 the "catch-all" case of canonical structures has a priority lower than     
 constant expansion. However, it is undesireable that local abbreviations   
 be opaque for the direct-sum predicate, e.g., not be able to handle        
 let S := (\sum_(i | P i) LargeExpression i)%MS in mxdirect S -> ...).      
   As in "quote", we use the interleaving of constant expansion and         
 canonical projection matching to achieve our goal: we use a "wrapper" type 
 (indeed, the wrapped T type defined in ssrfun.v) with a self-inserting     
 non-primitive constructor to gain finer control over the type and          
 structure inference process. The innermost, primitive, constructor flags   
 trivial sums; it is initially hidden by an eta-expansion, which has been   
 made into a (default) canonical structure -- this lets type inference      
 automatically insert this outer tag.                                       
   In detail, we define three types                                         
  mxsum_spec S r <-> There exists a finite list of matrices A1, ..., Ak     
                     such that S is the set sum of the Ai, and r is the sum 
                     of the ranks of the Ai, i.e., S = (A1 + ... + Ak)%MS   
                     and r = \rank A1 + ... + \rank Ak. Note that           
                     mxsum_spec is a recursive dependent predicate family   
                     whose elimination rewrites simultaneaously S, r and    
                     the height of S.                                       
   proper_mxsum_expr n == The interface for proper sum expressions; this is 
                     a double-entry interface, keyed on both the matrix sum 
                     value and the rank sum. The matrix value is restricted 
                     to square matrices, as the "+"%MS operator always      
                     returns a square matrix. This interface has two        
                     canonical insances, for binary and n-ary sums.         
   mxsum_expr m n == The interface for general sum expressions, comprising  
                     both proper sums and trivial sums consisting of a      
                     single matrix. The key values are WRAPPED as this lets 
                     us give priority to the "proper sum" interpretation    
                     (see below). To allow for trivial sums, the matrix key 
                     can have any dimension. The mxsum_expr interface has   
                     two canonical instances, for trivial and proper sums,  
                     keyed to the Wrap and wrap constructors, respectively. 
 The projections for the two interfaces above are                           
   proper_mxsum_val, mxsum_val : these are respectively coercions to 'M_n   
                     and wrapped 'M_(m, n); thus, the matrix sum for an     
                     S : mxsum_expr m n can be written unwrap S.            
   proper_mxsum_rank, mxsum_rank : projections to the nat and wrapped nat,  
                     respectively; the rank sum for S : mxsum_expr m n is   
                     thus written unwrap (mxsum_rank S).                    
 The mxdirect A predicate actually gets A in a phantom argument, which is   
 used to infer an (implicit) S : mxsum_expr such that unwrap S = A; the     
 actual definition is \rank (unwrap S) == unwrap (mxsum_rank S).            
   Note that the inference of S is inherently ambiguous: ANY matrix can be  
 viewed as a trivial sum, including one whose description is manifestly a   
 proper sum. We use the wrapped type and the interaction between delta      
 reduction and canonical structure inference to resolve this ambiguity in   
 favor of proper sums, as follows:                                          
    - The phantom type sets up a unification problem of the form            
         unwrap (mxsum_val ?S) = A                                          
      with unknown evar ?S : mxsum_expr m n.                                
    - As the constructor wrap is also a default Canonical Structure for the 
      wrapped type, so A is immediately replaced with unwrap (wrap A) and   
      we get the residual unification problem                               
         mxsum_val ?S = wrap A                                              
    - Now Coq tries to apply the proper sum Canonical Structure, which has  
      key projection wrap (proper_mxsum_val ?PS) where ?PS is a fresh evar  
      (of type proper_mxsum_expr n). This can only succeed if m = n, and if 
      a solution can be found to the recursive unification problem          
         proper_mxsum_val ?PS = A                                           
      This causes Coq to look for one of the two canonical constants for    
      proper_mxsum_val (addsmx or bigop) at the head of A, delta-expanding  
      A as needed, and then inferring recursively mxsum_expr structures for 
      the last argument(s) of that constant.                                
    - If the above step fails then the wrap constant is expanded, revealing 
      the primitive Wrap constructor; the unification problem now becomes   
         mxsum_val ?S = Wrap A                                              
      which fits perfectly the trivial sum canonical structure, whose key   
      projection is Wrap ?B where ?B is a fresh evar. Thus the inference    
      succeeds, and returns the trivial sum.                                
 Note that the rank projections also register canonical values, so that the 
 same process can be used to infer a sum structure from the rank sum. In    
 that case, however, there is no ambiguity and the inference can fail,      
 because the rank sum for a trivial sum is not an arbitrary integer -- it   
 must be of the form \rank ?B. It is nevertheless necessary to use the      
 wrapped nat type for the rank sums, because in the non-trivial case the    
 head constant of the nat expression is determined by the proper_mxsum_expr 
 canonical structure, so the mxsum_expr structure must use a generic        
 constant, namely wrap.                                                     

Inductive mxsum_spec n : forall m, 'M[F]_(m, n) -> nat -> Prop :=
 | TrivialMxsum m 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.

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

Canonical Structure trivial_mxsum m n 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;
  _ : mxsum_spec proper_mxsum_val proper_mxsum_rank
}.

Definition proper_mxsumP n (S : proper_mxsum_expr n) :=
  let: ProperMxsumExpr _ _ termS := S return mxsum_spec S (proper_mxsum_rank S)
  in termS.

Canonical Structure sum_mxsum n (S : proper_mxsum_expr n) :=
  @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).
Fact binary_mxsum_proof :
  mxsum_spec (unwrap S1 + unwrap S2)
             (unwrap (mxsum_rank S1) + unwrap (mxsum_rank S2)).
Canonical Structure binary_mxsum_expr := ProperMxsumExpr binary_mxsum_proof.
End Binary.

Section Nary.
Variables (P : pred I) (n : nat) (S_ : I -> mxsum_expr n n).
Fact nary_mxsum_proof :
  mxsum_spec (\sum_(i | P i) unwrap (S_ i))
             (\sum_(i | P i) unwrap (mxsum_rank (S_ i))).
Canonical Structure 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).

End SumExpr.

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

Lemma mxdirectP : forall n (S : proper_mxsum_expr n),
  reflect (\rank S = proper_mxsum_rank S) (mxdirect S).
Implicit Arguments mxdirectP [n S].

Lemma mxdirect_trivial : forall m n A,
  mxdirect (unwrap (@trivial_mxsum m n A)).

Lemma mxrank_sum_leqif : forall m n (S : mxsum_expr m n),
  \rank (unwrap S) <= unwrap (mxsum_rank S) ?= iff mxdirect (unwrap S).

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

Lemma mxdirectEgeq : forall m n (S : mxsum_expr m n),
  mxdirect (unwrap S) = (\rank (unwrap S) >= unwrap (mxsum_rank S)).

Section BinaryDirect.

Variables m1 m2 n : nat.

Lemma mxdirect_addsE : forall (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.

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

End BinaryDirect.

Section NaryDirect.

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


Let mxdirect_sums_recP : forall S_ : I -> mxsum_expr n n,
  reflect (forall i, P i -> mxdirect (unwrap (S_ i)) /\ TIsum (unwrap \o S_) i)
          (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).

Lemma mxdirect_sumsP : forall A_ : I -> 'M_n,
  reflect (forall 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 : forall (S_ : I -> mxsum_expr n n) (xunwrap := unwrap),
  reflect (and (forall 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.

Section SubDaddsmx.

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
                        & forall 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.

End SubDaddsmx.

Section SubDsumsmx.

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 forall i, P i -> (A_ i <= B i)%MS
                        & A = \sum_(i | P i) A_ i
                        & forall C, (forall 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 ->
  sub_dsumsmx_spec.

End SubDsumsmx.

Section Eigenspace.

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

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

Lemma eigenspaceP : forall a m (W : 'M_(m, n)),
  reflect (W *m g = a *: W) (W <= eigenspace a)%MS.

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

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

End Eigenspace.

End RowSpaceTheory.

Hint Resolve submx_refl.
Implicit Arguments submxP [F m1 m2 n A B].
Implicit Arguments eq_row_sub [F m n v A].
Implicit Arguments row_subP [F m1 m2 n A B].
Implicit Arguments rV_subP [F m1 m2 n A B].
Implicit Arguments row_subPn [F m1 m2 n A B].
Implicit Arguments sub_rVP [F n u v].
Implicit Arguments rV_eqP [F m1 m2 n A B].
Implicit Arguments rowV0Pn [F m n A].
Implicit Arguments rowV0P [F m n A].
Implicit Arguments eqmx0P [F m n A].
Implicit Arguments row_fullP [F m n A].
Implicit Arguments row_freeP [F m n A].
Implicit Arguments eqmxP [F m1 m2 n A B].
Implicit Arguments genmxP [F m1 m2 n A B].
Implicit Arguments addsmx_idPr [F m1 m2 n A B].
Implicit Arguments addsmx_idPl [F m1 m2 n A B].
Implicit Arguments sub_addsmxP [F m1 m2 m3 n A B C].
Implicit Arguments sumsmx_sup [F I P m n A B_].
Implicit Arguments sumsmx_subP [F I P m n A_ B].
Implicit Arguments sub_sumsmxP [F I P m n A B_].
Implicit Arguments sub_kermxP [F p m n A B].
Implicit Arguments det0P [F n A].
Implicit Arguments capmx_idPr [F m1 m2 n A B].
Implicit Arguments capmx_idPl [F m1 m2 n A B].
Implicit Arguments bigcapmx_inf [F I P m n A_ B].
Implicit Arguments sub_bigcapmxP [F I P m n A B_].
Implicit Arguments mxrank_injP [F m n A f].
Implicit Arguments mxdirectP [F n S].
Implicit Arguments mxdirect_addsP [F m1 m2 n A B].
Implicit Arguments mxdirect_sumsP [F I P n A_].
Implicit Arguments mxdirect_sumsE [F I P n S_].
Implicit Arguments eigenspaceP [F n g a m W].
Implicit Arguments eigenvalueP [F n g a].

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_ ( <- r | P ) B" :=
  (\big[addsmx/0%R]_(<- r | P%B) B%MS) : matrix_set_scope.
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_ ( <- r | P ) B" :=
  (\big[capmx/1%:M]_(<- r | P%B) 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 CardGL.

Variable F : finFieldType.

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

 An alternate, somewhat more elementary proof, that does not rely on the 
 row-space theory, but directly performs the LUP decomposition.          
Lemma LUP_card_GL : forall 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_2 : #|'GL_2[F]| = (#|F| * #|F|.-1 ^ 2 * #|F|.+1)%N.

End CardGL.

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

Section MatrixAlgebra.

Variables F : fieldType.

Local Notation "A \in R" := (@submx F _ _ _ (mxvec A) R).

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

Lemma memmx0 : forall n A, (A \in (0 : 'A_n)) -> A = 0.

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

Lemma memmx_subP : forall m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
  reflect (forall A, A \in R1 -> A \in R2) (R1 <= R2)%MS.
Implicit Arguments memmx_subP [m1 m2 n R1 R2].

Lemma memmx_eqP : forall m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
  reflect (forall A, (A \in R1) = (A \in R2)) (R1 == R2)%MS.
Implicit Arguments memmx_eqP [m1 m2 n R1 R2].

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

Lemma memmx_sumsP : forall (I : finType) (P : pred I) n (A : 'M_n) R_,
  reflect (exists2 A_, A = \sum_(i | P i) A_ i & forall i, A_ i \in R_ i)
          (A \in \sum_(i | P i) R_ i)%MS.
Implicit Arguments memmx_sumsP [I P n A R_].

Lemma has_non_scalar_mxP : forall 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.


Local Notation "R1 * R2" := (mulsmx R1 R2) : matrix_set_scope.

Lemma genmx_muls : forall m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
  <<(R1 * R2)%MS>>%MS = (R1 * R2)%MS.

Lemma mem_mulsmx : forall 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 : forall m1 m2 m n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
                    forall (R : 'A_(m, n)),
  reflect (forall A1 A2, A1 \in R1 -> A2 \in R2 -> A1 *m A2 \in R)
          (R1 * R2 <= R)%MS.
Implicit Arguments mulsmx_subP [m1 m2 m n R1 R2 R].

Lemma mulsmxS : forall m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
                forall (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)),
  (R1 <= R3 -> R2 <= R4 -> R1 * R2 <= R3 * R4)%MS.

Lemma muls_eqmx : forall m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
                  forall (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)),
  (R1 :=: R3 -> R2 :=: R4 -> R1 * R2 = R3 * R4)%MS.

Lemma mulsmxP : forall m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)),
  reflect (exists2 A1, forall i, A1 i \in R1 & exists2 A2, forall i, A2 i \in R2
           & A = \sum_(i < n ^ 2) A1 i *m A2 i)
          (A \in R1 * R2)%MS.
Implicit Arguments mulsmxP [m1 m2 n A R1 R2].

Lemma mulsmxA : forall m1 m2 m3 n (R1 : 'A_(m1, n)),
                forall (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)),
  (R1 * (R2 * R3) = R1 * R2 * R3)%MS.

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

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

Lemma mulsmx0 : forall m1 m2 n (R1 : 'A_(m1, n)),
  (R1 * (0 : 'A_(m2, n)) = 0)%MS.

Lemma muls0mx : forall 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 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 mxring_id m n (R : 'A_(m, n)) e :=
  [/\ e != 0,
      e \in R,
      forall A, A \in R -> e *m A = A
    & forall A, A \in R -> A *m e = A]%MS.

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.

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

Lemma mxring_idP : forall m n (R : 'A_(m, n)),
  reflect (exists e, mxring_id R e) (has_mxring_id R).
Implicit Arguments mxring_idP [m n R].

Section CentMxDef.

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).

Lemma cent_mx_fun_is_linear : linear cent_mx_fun.
Canonical Structure cent_mx_fun_additive := Additive cent_mx_fun_is_linear.
Canonical Structure cent_mx_fun_linear := Linear cent_mx_fun_is_linear.

Definition cent_mx := kermx (lin_mx cent_mx_fun).

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

End CentMxDef.

Local Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope.
Local Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.

Lemma cent_rowP : forall m n B (R : 'A_(m, n)),
  reflect (forall i (A := vec_mx (row i R)), A *m B = B *m A) (B \in 'C(R))%MS.
Implicit Arguments cent_rowP [m n B R].

Lemma cent_mxP : forall m n B (R : 'A_(m, n)),
  reflect (forall A, A \in R -> A *m B = B *m A) (B \in 'C(R))%MS.
Implicit Arguments cent_mxP [m n B R].

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

Lemma center_mx_sub : forall m n (R : 'A_(m, n)), ('Z(R) <= R)%MS.

Lemma center_mxP : forall m n A (R : 'A_(m, n)),
  reflect (A \in R /\ forall B, B \in R -> B *m A = A *m B)
          (A \in 'Z(R))%MS.
Implicit Arguments center_mxP [m n A R].

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

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

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

Lemma mxdirect_adds_center : forall 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 : forall (I : finType) m n (R : 'A_(m, n)) R_,
    (\sum_i R_ i :=: R)%MS -> mxdirect (\sum_i R_ i) ->
    (forall i : I, mx_ideal R (R_ i)) ->
  ('Z(R) :=: \sum_i 'Z(R_ i))%MS.

End MatrixAlgebra.



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.

Implicit Arguments memmx_subP [F m1 m2 n R1 R2].
Implicit Arguments memmx_eqP [F m1 m2 n R1 R2].
Implicit Arguments memmx_addsP [F m1 m2 n R1 R2].
Implicit Arguments memmx_sumsP [F I P n A R_].
Implicit Arguments mulsmx_subP [F m1 m2 m n R1 R2 R].
Implicit Arguments mulsmxP [F m1 m2 n A R1 R2].
Implicit Arguments mxring_idP [m n R].
Implicit Arguments cent_rowP [F m n B R].
Implicit Arguments cent_mxP [F m n B R].
Implicit Arguments center_mxP [F m n A R].

 Parametricity for the row-space/F-algebra theory.                         
Section MapMatrixSpaces.

Variables (aF rF : fieldType) (f : {rmorphism aF -> rF}).
Local Notation "A ^f" := (map_mx f A) : ring_scope.

Lemma gaussian_elimination_map : forall m n (A : 'M_(m, n)),
  gaussian_elimination A^f = ((col_ebase A)^f, (row_ebase A)^f, \rank A).

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

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

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

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

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

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

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

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

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

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

Lemma map_submx : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  (A^f <= B^f)%MS = (A <= B)%MS.

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

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

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

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

Let map_capmx_gen : forall 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 : forall m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)),
  ((A :&: B)^f :=: A^f :&: B^f)%MS.

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

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

Lemma map_eigenspace : forall n (g : 'M_n) a,
  (eigenspace g a)^f = eigenspace g^f (f a).

Lemma eigenvalue_map : forall n (g : 'M_n) a,
  eigenvalue g^f (f a) = eigenvalue g a.

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

Lemma map_mulsmx : forall m1 m2 n (E1 : 'A_(m1, n)) (E2 : 'A_(m2, n)),
  ((E1 * E2)%MS^f :=: E1^f * E2^f)%MS.

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

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

End MapMatrixSpaces.