Library mathcomp.algebra.mxalgebra
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype finfun bigop finset fingroup perm order.
From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype finfun bigop finset fingroup perm order.
From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix.
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).
maxrankfun A == injective function f so that rowsub f A is a submatrix
of A with the same rank as A.
fullrankfun fA == injective function f so that rowsub f A is row full,
where fA is a proof of row_full A
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, where
capmx_gen A B is a rectangular matrix equivalent to
(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
parallel 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.
stablemx V f <=> the matrix f represents an endomorphism that preserves V
:= (V *m f <= V)%MS
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.
Set Implicit Arguments.
Declare Scope matrix_set_scope.
Import GroupScope.
Import GRing.Theory.
Local Open Scope ring_scope.
Reserved Notation "\rank A" (at level 10, A at level 8, format "\rank A").
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.
Rank and row-space theory *****************************
Decomposition with double pivoting; computes the rank, row and column
images, kernels, and complements of a matrix.
Fixpoint Gaussian_elimination_ {F : fieldType} {m n} : 'M[F]_(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
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)
| _, _ ⇒ fun _ ⇒ (1%:M, 1%:M, 0)
end.
Canonical Gaussian_elimination_unlockable := Unlockable Gaussian_elimination.unlock.
Canonical mxrank_unlockable := Unlockable mxrank.unlock.
Section RowSpaceTheoryDefs.
Variable F : fieldType.
Implicit Types m n p r : nat.
Variables (m n : nat) (A : 'M_(m, n)).
Let LUr := @Gaussian_elimination F m n A.
Definition col_ebase := LUr.1.1.
Definition row_ebase := LUr.1.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 RowSpaceTheoryDefs.
Implicit Types F : fieldType.
Canonical submx_unlockable := Unlockable submx.unlock.
Arguments mxrank {F} {m%N n%N} A%MS.
Arguments complmx {F} {m%N n%N} A%MS.
Arguments submx {F} {m1%N m2%N n%N} A%MS B%MS : rename.
Definition ltmx F m1 m2 n (A : 'M[F]_(m1, n)) (B : 'M_(m2, n)) :=
(A ≤ B)%MS && ~~ (B ≤ A)%MS.
Arguments ltmx {F} {m1%N m2%N n%N} A%MS B%MS.
Definition eqmx F m1 m2 n (A : 'M[F]_(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.
Arguments eqmx {F} {m1%N m2%N n%N} A%MS B%MS.
Notation stablemx V f := (V%MS ×m f%R ≤ V%MS)%MS.
Section LtmxIdentities.
Variable F : fieldType.
Implicit Types m n p r : nat.
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.
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.
Canonical addsmx_unlockable := Unlockable addsmx.unlock.
Arguments addsmx {F} {m1%N m2%N n%N} A%MS B%MS : rename.
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.
Definition capmx_gen F m1 m2 n (A : 'M[F]_(m1, n)) (B : 'M_(m2, n)) :=
lsubmx (kermx (col_mx A B)) ×m A.
Canonical capmx_unlockable := Unlockable capmx.unlock.
Arguments capmx {F} {m1%N m2%N n%N} A%MS B%MS : rename.
Canonical diffmx_unlockable := Unlockable diffmx.unlock.
Arguments diffmx {F} {m1%N m2%N n%N} A%MS B%MS : rename.
Section RowSpaceTheory.
Variable F : fieldType.
Implicit Types m n p r : nat.
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.
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 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 eq_row_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
(A :=: B)%MS → row_full A = row_full B.
Let unitmx1F := @unitmx1 F.
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 : 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_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.
Arguments mulmx1_min_rank [r m n A].
Lemma mulmx_max_rank r m n (M : 'M_(m, r)) (N : 'M_(r, n)) :
\rank (M ×m N) ≤ r.
Arguments mulmx_max_rank [r m n].
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 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 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_opp m n (A : 'M_(m, n)) : \rank (- A) = \rank A.
Lemma mxrank0 m n : \rank (0 : 'M_(m, n)) = 0%N.
Lemma mxrank_eq0 m n (A : 'M_(m, n)) : (\rank A == 0) = (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 mulmxKpV m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
(A ≤ B)%MS → A ×m pinvmx B ×m B = A.
Lemma mulmxVp m n (A : 'M[F]_(m, n)) : row_free A → A ×m pinvmx A = 1%:M.
Lemma mulmxKp p m n (B : 'M[F]_(m, n)) : row_free B →
cancel ((@mulmx _ p _ _)^~ B) (mulmx^~ (pinvmx B)).
Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
reflect (∃ D, A = D ×m B) (A ≤ B)%MS.
Arguments submxP {m1 m2 n A B}.
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 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 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.
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.
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.
Lemma ltmx_trans m n : transitive (@ltmx F m m n).
Lemma ltmx_irrefl m n : irreflexive (@ltmx F m m n).
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 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 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 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 rowsub_sub m1 m2 n (f : 'I_m2 → 'I_m1) (A : 'M_(m1, n)) :
(rowsub f A ≤ A)%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 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.
Arguments eq_row_sub [m n v A].
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.
Arguments row_subP {m1 m2 n A B}.
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.
Arguments rV_subP {m1 m2 n A B}.
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[F]_n) : reflect (∃ a, u = a *: v) (u ≤ v)%MS.
Lemma rank_rV n (v : 'rV[F]_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 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 row_fullP m n (A : 'M_(m, n)) :
reflect (∃ B, B ×m A = 1%:M) (row_full A).
Arguments row_fullP {m n A}.
Lemma row_full_inj m n p A : row_full A → injective (@mulmx F 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_free_inj m n p A : row_free A → injective ((@mulmx F m n p)^~ A).
A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~
but which is canonically additive
Definition row_free_injr m n p A : row_free A → injective (mulmxr A) :=
@row_free_inj m n p A.
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 mxrank_unit n (A : 'M_n) : A \in unitmx → \rank A = 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.
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 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 lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false.
Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx → pinvmx A = invmx A.
Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A → pinvmx A ×m A = 1%:M.
Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A → row_free (pinvmx A).
Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A → row_full (pinvmx A).
Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
reflect (A :=: B)%MS (A == B)%MS.
Arguments eqmxP {m1 m2 n A B}.
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_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_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 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 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_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 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 eq_row_base m n (A : 'M_(m, n)) : (row_base A :=: A)%MS.
Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0.
Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M).
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 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.
Arguments genmxP {m1 m2 n A B}.
Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.
Lemma genmx1 n : <<1%:M : 'M_n>>%MS = 1%:M.
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 mxrank_gen m n (A : 'M_(m, n)) : \rank <<A>>%MS = \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 : 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_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 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 row_full_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_full (castmx e A : 'M_(m2, n)) = row_full A.
Lemma row_free_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_free (castmx e A : 'M_(m2, n)) = row_free A.
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.
Lemma rowsub_comp_sub (m n p q : nat) f (g : 'I_n → 'I_p) (A : 'M_(m, q)) :
(rowsub (f \o g) A ≤ rowsub f A)%MS.
Lemma submx_rowsub (m n p q : nat) (h : 'I_n → 'I_p) f g (A : 'M_(m, q)) :
f =1 g \o h → (rowsub f A ≤ rowsub g A)%MS.
Arguments submx_rowsub [m1 m2 m3 n] h [f g A] _ : rename.
Lemma eqmx_rowsub_comp_perm (m1 m2 n : nat) (s : 'S_m2) f (A : 'M_(m1, n)) :
(rowsub (f \o s) A :=: rowsub f A)%MS.
Lemma eqmx_rowsub_comp (m n p q : nat) f (g : 'I_n → 'I_p) (A : 'M_(m, q)) :
p ≤ n → injective g → (rowsub (f \o g) A :=: rowsub f A)%MS.
Lemma eqmx_rowsub (m n p q : nat) (h : 'I_n → 'I_p) f g (A : 'M_(m, q)) :
injective h → p ≤ n → f =1 g \o h → (rowsub f A :=: rowsub g A)%MS.
Arguments eqmx_rowsub [m1 m2 m3 n] h [f g A] _ : rename.
Section AddsmxSub.
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 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 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 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.
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_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 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 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 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 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_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 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.
Arguments sub_addsmxP {m1 m2 m3 n A B C}.
Variable I : finType.
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 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.
Arguments sumsmx_sup i0 [P m n A B_].
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 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 sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I → 'M_(n, p)) :
reflect (∃ u_ : I → 'M_(m, n), 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 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_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_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 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 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 sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
reflect (B ×m A = 0) (B ≤ kermx A)%MS.
Lemma sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
(B ≤ kermx A)%MS = (B ×m A == 0).
Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS.
Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
row_free B → (A ×m B == 0) = (A == 0).
Lemma inj_row_free m n (A : 'M_(m, n)) :
(∀ v : 'rV_m, v ×m A = 0 → v = 0) → row_free A.
Lemma row_freePn m n (M : 'M[F]_(m, n)) :
reflect (∃ i, (row i M ≤ row' i M)%MS) (~~ row_free M).
Lemma negb_row_free m n (M : 'M[F]_(m, n)) :
~~ row_free M = [∃ i, (row i M ≤ row' i M)%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 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 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.
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_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 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 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 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 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 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 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 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 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 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.
Lemma cap1mx n (A : 'M_n) : (1%:M :&: A = 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 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 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 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_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 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_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 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 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 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_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.
@row_free_inj m n p A.
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 mxrank_unit n (A : 'M_n) : A \in unitmx → \rank A = 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.
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 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 lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false.
Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx → pinvmx A = invmx A.
Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A → pinvmx A ×m A = 1%:M.
Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A → row_free (pinvmx A).
Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A → row_full (pinvmx A).
Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
reflect (A :=: B)%MS (A == B)%MS.
Arguments eqmxP {m1 m2 n A B}.
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_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_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 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 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_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 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 eq_row_base m n (A : 'M_(m, n)) : (row_base A :=: A)%MS.
Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0.
Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M).
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 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.
Arguments genmxP {m1 m2 n A B}.
Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.
Lemma genmx1 n : <<1%:M : 'M_n>>%MS = 1%:M.
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 mxrank_gen m n (A : 'M_(m, n)) : \rank <<A>>%MS = \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 : 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_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 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 row_full_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_full (castmx e A : 'M_(m2, n)) = row_full A.
Lemma row_free_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_free (castmx e A : 'M_(m2, n)) = row_free A.
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.
Lemma rowsub_comp_sub (m n p q : nat) f (g : 'I_n → 'I_p) (A : 'M_(m, q)) :
(rowsub (f \o g) A ≤ rowsub f A)%MS.
Lemma submx_rowsub (m n p q : nat) (h : 'I_n → 'I_p) f g (A : 'M_(m, q)) :
f =1 g \o h → (rowsub f A ≤ rowsub g A)%MS.
Arguments submx_rowsub [m1 m2 m3 n] h [f g A] _ : rename.
Lemma eqmx_rowsub_comp_perm (m1 m2 n : nat) (s : 'S_m2) f (A : 'M_(m1, n)) :
(rowsub (f \o s) A :=: rowsub f A)%MS.
Lemma eqmx_rowsub_comp (m n p q : nat) f (g : 'I_n → 'I_p) (A : 'M_(m, q)) :
p ≤ n → injective g → (rowsub (f \o g) A :=: rowsub f A)%MS.
Lemma eqmx_rowsub (m n p q : nat) (h : 'I_n → 'I_p) f g (A : 'M_(m, q)) :
injective h → p ≤ n → f =1 g \o h → (rowsub f A :=: rowsub g A)%MS.
Arguments eqmx_rowsub [m1 m2 m3 n] h [f g A] _ : rename.
Section AddsmxSub.
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 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 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 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.
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_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 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 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 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 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_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 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.
Arguments sub_addsmxP {m1 m2 m3 n A B C}.
Variable I : finType.
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 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.
Arguments sumsmx_sup i0 [P m n A B_].
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 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 sub_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I → 'M_(n, p)) :
reflect (∃ u_ : I → 'M_(m, n), 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 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_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_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 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 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 sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
reflect (B ×m A = 0) (B ≤ kermx A)%MS.
Lemma sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
(B ≤ kermx A)%MS = (B ×m A == 0).
Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS.
Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
row_free B → (A ×m B == 0) = (A == 0).
Lemma inj_row_free m n (A : 'M_(m, n)) :
(∀ v : 'rV_m, v ×m A = 0 → v = 0) → row_free A.
Lemma row_freePn m n (M : 'M[F]_(m, n)) :
reflect (∃ i, (row i M ≤ row' i M)%MS) (~~ row_free M).
Lemma negb_row_free m n (M : 'M[F]_(m, n)) :
~~ row_free M = [∃ i, (row i M ≤ row' i M)%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 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 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.
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_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 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 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 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 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 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 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 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 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 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.
Lemma cap1mx n (A : 'M_n) : (1%:M :&: A = 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 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 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 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_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 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_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 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 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 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_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.
rank of block matrices with 0s inside
Lemma rank_col_mx0 m n p (A : 'M_(m, n)) :
\rank (col_mx A (0 : 'M_(p, n))) = \rank A.
Lemma rank_col_0mx m n p (A : 'M_(m, n)) :
\rank (col_mx (0 : 'M_(p, n)) A) = \rank A.
Lemma rank_row_mx0 m n p (A : 'M_(m, n)) :
\rank (row_mx A (0 : 'M_(m, p))) = \rank A.
Lemma rank_row_0mx m n p (A : 'M_(m, n)) :
\rank (row_mx (0 : 'M_(m, p)) A) = \rank A.
Lemma rank_diag_block_mx m n p q
(A : 'M_(m, n)) (B : 'M_(p, q)) :
\rank (block_mx A 0 0 B) = (\rank A + \rank B)%N.
Subspace projection matrix
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_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 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.
Completing a partially injective matrix to get a unit matrix.
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.
Mapping between two subspaces with the same dimension.
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.
maximal rank and full rank submatrices
Section MaxRankSubMatrix.
Variables (m n : nat) (A : 'M_(m, n)).
Definition maxrankfun : 'I_m ^ \rank A :=
[arg max_(f > finfun (widen_ord (rank_leq_row A))) \rank (rowsub f A)].
Lemma maxrowsub_free : row_free (rowsub mxf A).
Lemma eq_maxrowsub : (rowsub mxf A :=: A)%MS.
Lemma maxrankfun_inj : injective mxf.
Variable (rkA : row_full A).
Lemma maxrowsub_full : row_full (rowsub mxf A).
Hint Resolve maxrowsub_full : core.
Definition fullrankfun : 'I_m ^ n := finfun (mxf \o cast_ord (esym (eqP rkA))).
Lemma fullrowsub_full : row_full (rowsub frf A).
Lemma fullrowsub_unit : rowsub frf A \in unitmx.
Lemma fullrowsub_free : row_free (rowsub frf A).
Lemma mxrank_fullrowsub : \rank (rowsub frf A) = n.
Lemma eq_fullrowsub : (rowsub frf A :=: A)%MS.
Lemma fullrankfun_inj : injective frf.
End MaxRankSubMatrix.
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 instance 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 instance, 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.
Inductive mxsum_spec n : ∀ 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.
Arguments mxsum_spec {n%N m%N} T%MS r%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 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 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 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).
Fact nary_mxsum_proof :
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).
End SumExpr.
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).
Arguments mxdirectP {n S}.
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).
Lemma mxdirectE m n (S : mxsum_expr m n) :
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)).
Section BinaryDirect.
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.
Lemma mxdirect_addsP (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 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)))).
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)))).
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)).
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.
End SubDaddsmx.
Section SubDsumsmx.
Variables (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B : I → 'M[F]_n).
Variant sub_dsumsmx_spec : Prop :=
SubDsumsmxSpec A_ of ∀ i, P i → (A_ i ≤ B i)%MS
&