Merge pull request #574 from CohenCyril/mxsub

Submatrix theory

3 files changed, 292 insertions, 1 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 70f28ec..59ffda2 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -54,6 +54,13 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
 (*                   should be decomposed.                                    *)
 (*   [u|d]submx A == the up/down submatrices of a column block matrix A.      *)
 (* [u|d][l|r]submx A == the upper left, etc submatrices of a block matrix A.  *)
+(*    mxsub f g A == generic reordered submatrix, given by functions f and g  *)
+(*                   which specify which subset of rows and columns to take   *)
+(*                   and how to reorder them, e.g. picking f and g to be      *)
+(*                   increasing yields traditional submatrices.               *)
+(*                := \matrix_(i, j) A (f i) (g i)                             *)
+(*     rowsub f A := mxsub f id A                                             *)
+(*     colsub g A := mxsub id g A                                             *)
 (* castmx eq_mn A == A : 'M_(m, n) cast to 'M_(m', n') using the equation     *)
 (*                   pair eq_mn : (m = m') * (n = n'). This is the usual      *)
 (*                   workaround for the syntactic limitations of dependent    *)
@@ -351,6 +358,11 @@ Definition col j0 A := \col_i A i j0.
 Definition row' i0 A := \matrix_(i, j) A (lift i0 i) j.
 Definition col' j0 A := \matrix_(i, j) A i (lift j0 j).
 
+(* reindexing/subindex a matrix *)
+Definition mxsub m' n' f g A := \matrix_(i < m', j < n') A (f i) (g j).
+Local Notation colsub g := (mxsub id g).
+Local Notation rowsub f := (mxsub f id).
+
 Lemma castmx_const m' n' (eq_mn : (m = m') * (n = n')) a :
   castmx eq_mn (const_mx a) = const_mx a.
 Proof. by case: eq_mn; case: m' /; case: n' /. Qed.
@@ -413,8 +425,62 @@ Lemma col_row_permC s t A :
   col_perm s (row_perm t A) = row_perm t (col_perm s A).
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 
+Lemma rowEsub i : row i = rowsub (fun=> i). Proof. by []. Qed.
+Lemma colEsub j : col j = colsub (fun=> j). Proof. by []. Qed.
+
+Lemma row'Esub i : row' i = rowsub (lift i). Proof. by []. Qed.
+Lemma col'Esub j : col' j = colsub (lift j). Proof. by []. Qed.
+
+Lemma row_permEsub s : row_perm s = rowsub s.
+Proof. by rewrite /row_perm /mxsub !unlock. Qed.
+
+Lemma col_permEsub s : col_perm s = colsub s.
+Proof. by rewrite /col_perm /mxsub !unlock. Qed.
+
+Lemma xrowEsub i1 i2 : xrow i1 i2 = rowsub (tperm i1 i2).
+Proof. exact: row_permEsub. Qed.
+
+Lemma xcolEsub j1 j2 : xcol j1 j2 = colsub (tperm j1 j2).
+Proof. exact: col_permEsub. Qed.
+
+Lemma mxsub_id : mxsub id id =1 id.
+Proof. by move=> A; apply/matrixP => i j; rewrite !mxE. Qed.
+
+Lemma eq_mxsub m' n' f f' g g' : f =1 f' -> g =1 g' ->
+  @mxsub m' n' f g =1 mxsub f' g'.
+Proof. by move=> eq_f eq_g A; apply/matrixP => i j; rewrite !mxE eq_f eq_g. Qed.
+
+Lemma eq_rowsub m' (f f' : 'I_m' -> 'I_m) : f =1 f' -> rowsub f =1 rowsub f'.
+Proof. by move=> /eq_mxsub; apply. Qed.
+
+Lemma eq_colsub n' (g g' : 'I_n' -> 'I_n) : g =1 g' -> colsub g =1 colsub g'.
+Proof. by move=> /eq_mxsub; apply. Qed.
+
+Lemma mxsub_eq_id f g : f =1 id -> g =1 id -> mxsub f g =1 id.
+Proof. by move=> fid gid A; rewrite (eq_mxsub fid gid) mxsub_id. Qed.
+
+Lemma mxsub_eq_colsub n' f g : f =1 id -> @mxsub _ n' f g =1 colsub g.
+Proof. by move=> f_id; apply: eq_mxsub. Qed.
+
+Lemma mxsub_eq_rowsub m' f g : g =1 id -> @mxsub m' _ f g =1 rowsub f.
+Proof. exact: eq_mxsub. Qed.
+
+Lemma mxsub_ffunl m' n' f g : @mxsub m' n' (finfun f) g =1 mxsub f g.
+Proof. by apply: eq_mxsub => // i; rewrite ffunE. Qed.
+
+Lemma mxsub_ffunr m' n' f g : @mxsub m' n' f (finfun g) =1 mxsub f g.
+Proof. by apply: eq_mxsub => // i; rewrite ffunE. Qed.
+
+Lemma mxsub_ffun m' n' f g : @mxsub m' n' (finfun f) (finfun g) =1 mxsub f g.
+Proof. by move=> A; rewrite mxsub_ffunl mxsub_ffunr. Qed.
+
+Lemma mxsub_const m' n' f g a : @mxsub m' n' f g (const_mx a) = const_mx a.
+Proof. by apply/matrixP => i j; rewrite !mxE. Qed.
+
 End FixedDim.
 
+Local Notation colsub g := (mxsub id g).
+Local Notation rowsub f := (mxsub f id).
 Local Notation "A ^T" := (trmx A) : ring_scope.
 
 Lemma castmx_id m n erefl_mn (A : 'M_(m, n)) : castmx erefl_mn A = A.
@@ -524,6 +590,68 @@ Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 Lemma tr_col' m n j0 (A : 'M_(m, n)) : (col' j0 A)^T = row' j0 A^T.
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 
+Lemma mxsub_comp m1 m2 m3 n1 n2 n3
+  (f : 'I_m2 -> 'I_m1) (f' : 'I_m3 -> 'I_m2)
+  (g : 'I_n2 -> 'I_n1) (g' : 'I_n3 -> 'I_n2) (A : 'M_(m1, n1)) :
+  mxsub (f \o f') (g \o g') A = mxsub f' g' (mxsub f g A).
+Proof. by apply/matrixP => i j; rewrite !mxE. Qed.
+
+Lemma rowsub_comp m1 m2 m3 n
+  (f : 'I_m2 -> 'I_m1) (f' : 'I_m3 -> 'I_m2) (A : 'M_(m1, n)) :
+  rowsub (f \o f') A = rowsub f' (rowsub f A).
+Proof. exact: mxsub_comp. Qed.
+
+Lemma colsub_comp m n n2 n3
+  (g : 'I_n2 -> 'I_n) (g' : 'I_n3 -> 'I_n2) (A : 'M_(m, n)) :
+  colsub (g \o g') A = colsub g' (colsub g A).
+Proof. exact: mxsub_comp. Qed.
+
+Lemma mxsubrc m1 m2 n n2 f g (A : 'M_(m1, n)) :
+  mxsub f g A = rowsub f (colsub g A) :> 'M_(m2, n2).
+Proof. exact: mxsub_comp. Qed.
+
+Lemma mxsubcr m1 m2 n n2 f g (A : 'M_(m1, n)) :
+  mxsub f g A = colsub g (rowsub f A) :> 'M_(m2, n2).
+Proof. exact: mxsub_comp. Qed.
+
+Lemma rowsub_cast m1 m2 n (eq_m : m1 = m2) (A : 'M_(m2, n)) :
+  rowsub (cast_ord eq_m) A = castmx (esym eq_m, erefl) A.
+Proof. by case: _ / eq_m in A *; apply: (mxsub_eq_id (cast_ord_id _)). Qed.
+
+Lemma colsub_cast m n1 n2 (eq_n : n1 = n2) (A : 'M_(m, n2)) :
+  colsub (cast_ord eq_n) A = castmx (erefl, esym eq_n) A.
+Proof. by case: _ / eq_n in A *; apply: (mxsub_eq_id _ (cast_ord_id _)). Qed.
+
+Lemma mxsub_cast m1 m2 n1 n2 (eq_m : m1 = m2) (eq_n : n1 = n2) A :
+  mxsub (cast_ord eq_m) (cast_ord eq_n) A = castmx (esym eq_m, esym eq_n) A.
+Proof. by rewrite mxsubrc rowsub_cast colsub_cast castmx_comp/= etrans_id. Qed.
+
+Lemma castmxEsub m1 m2 n1 n2 (eq_mn : (m1 = m2) * (n1 = n2)) A :
+  castmx eq_mn A = mxsub (cast_ord (esym eq_mn.1)) (cast_ord (esym eq_mn.2)) A.
+Proof. by rewrite mxsub_cast !esymK; case: eq_mn. Qed.
+
+Lemma trmx_mxsub m1 m2 n1 n2 f g (A : 'M_(m1, n1)) :
+  (mxsub f g A)^T = mxsub g f A^T :> 'M_(n2, m2).
+Proof. by apply/matrixP => i j; rewrite !mxE. Qed.
+
+Lemma row_mxsub m1 m2 n1 n2
+    (f : 'I_m2 -> 'I_m1) (g : 'I_n2 -> 'I_n1) (A : 'M_(m1, n1)) i :
+  row i (mxsub f g A) = row (f i) (colsub g A).
+Proof. by rewrite !rowEsub -!mxsub_comp. Qed.
+
+Lemma col_mxsub m1 m2 n1 n2
+    (f : 'I_m2 -> 'I_m1) (g : 'I_n2 -> 'I_n1) (A : 'M_(m1, n1)) i :
+ col i (mxsub f g A) = col (g i) (rowsub f A).
+Proof. by rewrite !colEsub -!mxsub_comp. Qed.
+
+Lemma row_rowsub m1 m2 n (f : 'I_m2 -> 'I_m1) (A : 'M_(m1, n)) i :
+  row i (rowsub f A) = row (f i) A.
+Proof. by rewrite row_mxsub mxsub_id. Qed.
+
+Lemma col_colsub m n1 n2 (g : 'I_n2 -> 'I_n1) (A : 'M_(m, n1)) i :
+  col i (colsub g A) = col (g i) A.
+Proof. by rewrite col_mxsub mxsub_id. Qed.
+
 Ltac split_mxE := apply/matrixP=> i j; do ![rewrite mxE | case: split => ?].
 
 Section CutPaste.
@@ -591,6 +719,18 @@ Proof. by rewrite mxE (unsplitK (inr _ _)). Qed.
 Lemma col_mxKd A1 A2 : dsubmx (col_mx A1 A2) = A2.
 Proof. by apply/matrixP=> i j; rewrite mxE col_mxEd. Qed.
 
+Lemma lsubmxEsub : lsubmx = colsub (lshift _).
+Proof. by rewrite /lsubmx /mxsub !unlock. Qed.
+
+Lemma rsubmxEsub : rsubmx = colsub (@rshift _ _).
+Proof. by rewrite /rsubmx /mxsub !unlock. Qed.
+
+Lemma usubmxEsub : usubmx = rowsub (lshift _).
+Proof. by rewrite /usubmx /mxsub !unlock. Qed.
+
+Lemma dsubmxEsub  : dsubmx = rowsub (@rshift _ _).
+Proof. by rewrite /dsubmx /mxsub !unlock. Qed.
+
 Lemma eq_row_mx A1 A2 B1 B2 : row_mx A1 A2 = row_mx B1 B2 -> A1 = B1 /\ A2 = B2.
 Proof.
 move=> eqAB; move: (congr1 lsubmx eqAB) (congr1 rsubmx eqAB).
@@ -783,6 +923,18 @@ Definition drsubmx := rsubmx (dsubmx A).
 Lemma submxK : block_mx ulsubmx ursubmx dlsubmx drsubmx = A.
 Proof. by rewrite /block_mx !hsubmxK vsubmxK. Qed.
 
+Lemma ulsubmxEsub : ulsubmx = mxsub (lshift _) (lshift _) A.
+Proof. by rewrite /ulsubmx lsubmxEsub usubmxEsub -mxsub_comp. Qed.
+
+Lemma dlsubmxEsub : dlsubmx = mxsub (@rshift _ _) (lshift _) A.
+Proof. by rewrite /dlsubmx lsubmxEsub dsubmxEsub -mxsub_comp. Qed.
+
+Lemma ursubmxEsub : ursubmx = mxsub (lshift _) (@rshift _ _) A.
+Proof. by rewrite /ursubmx rsubmxEsub usubmxEsub -mxsub_comp. Qed.
+
+Lemma drsubmxEsub : drsubmx = mxsub (@rshift _ _) (@rshift _ _) A.
+Proof. by rewrite /drsubmx rsubmxEsub dsubmxEsub -mxsub_comp. Qed.
+
 End CutBlock.
 
 Section CatBlock.
@@ -922,6 +1074,22 @@ Proof.
 by move=> P0 PS; elim=> [//|n IHn] A; rewrite -[A](@submxK 1 _ 1); apply: PS.
 Qed.
 
+Lemma mxsub_ind
+    (weight : forall m n, 'M[R]_(m, n) -> nat)
+    (sub : forall m n m' n', ('I_m' -> 'I_m) -> ('I_n' -> 'I_n) -> Prop)
+    (P : forall m n, 'M[R]_(m, n) -> Type) :
+    (forall m n (A : 'M[R]_(m, n)),
+      (forall m' n' f g, weight m' n' (mxsub f g A) < weight m n A ->
+                         sub m n m' n' f g ->
+                         P m' n' (mxsub f g A)) -> P m n A) ->
+  forall m n A, P m n A.
+Proof.
+move=> Psub m n A; have [k] := ubnP (weight m n A).
+elim: k => [//|k IHk] in m n A *.
+rewrite ltnS => lt_A_k; apply: Psub => m' n' f g lt_A'_A ?.
+by apply: IHk; apply: leq_trans lt_A_k.
+Qed.
+
 End Induction.
 
 (* Bijections mxvec : 'M_(m, n) <----> 'rV_(m * n) : vec_mx *)
@@ -987,6 +1155,12 @@ Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK.
 Arguments trmx_inj {R m n} [A1 A2] eqA12t : rename.
 
 Notation "A ^T" := (trmx A) : ring_scope.
+Notation colsub g := (mxsub id g).
+Notation rowsub f := (mxsub f id).
+
+Arguments eq_mxsub [R m n m' n' f] f' [g] g' _.
+Arguments eq_rowsub [R m n m' f] f' _.
+Arguments eq_colsub [R m n n' g] g' _.
 
 (* Matrix parametricity. *)
 Section MapMatrix.
@@ -1020,6 +1194,9 @@ Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 Lemma map_col' j0 : (col' j0 A)^f = col' j0 A^f.
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 
+Lemma map_mxsub m' n' g h : (@mxsub _ _ _  m' n' g h A)^f = mxsub g h A^f.
+Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
+
 Lemma map_row_perm s : (row_perm s A)^f = row_perm s A^f.
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
 
@@ -1193,6 +1370,7 @@ Canonical row_additive m n i := SwizzleAdd (@row V m n i).
 Canonical col_additive m n j := SwizzleAdd (@col V m n j).
 Canonical row'_additive m n i := SwizzleAdd (@row' V m n i).
 Canonical col'_additive m n j := SwizzleAdd (@col' V m n j).
+Canonical mxsub_additive m n m' n' f g := SwizzleAdd (@mxsub V m n m' n' f g).
 Canonical row_perm_additive m n s := SwizzleAdd (@row_perm V m n s).
 Canonical col_perm_additive m n s := SwizzleAdd (@col_perm V m n s).
 Canonical xrow_additive m n i1 i2 := SwizzleAdd (@xrow V m n i1 i2).
@@ -1595,6 +1773,7 @@ Canonical row_linear m n i := SwizzleLin (@row R m n i).
 Canonical col_linear m n j := SwizzleLin (@col R m n j).
 Canonical row'_linear m n i := SwizzleLin (@row' R m n i).
 Canonical col'_linear m n j := SwizzleLin (@col' R m n j).
+Canonical mxsub_linear m n m' n' f g := SwizzleLin (@mxsub R m n m' n' f g).
 Canonical row_perm_linear m n s := SwizzleLin (@row_perm R m n s).
 Canonical col_perm_linear m n s := SwizzleLin (@col_perm R m n s).
 Canonical xrow_linear m n i1 i2 := SwizzleLin (@xrow R m n i1 i2).
@@ -1899,6 +2078,18 @@ Proof.
 by apply/rowP=> j; rewrite mxE summxE; apply: eq_bigr => i _; rewrite !mxE.
 Qed.
 
+Lemma mxsub_mul m n m' n' p f g (A : 'M_(m, p)) (B : 'M_(p, n)) :
+  mxsub f g (A *m B) = rowsub f A *m colsub g B :> 'M_(m', n').
+Proof. by split_mxE; apply: eq_bigr => k _; rewrite !mxE. Qed.
+
+Lemma mul_rowsub_mx m n m' p f (A : 'M_(m, p)) (B : 'M_(p, n)) :
+  rowsub f A *m B = rowsub f (A *m B) :> 'M_(m', n).
+Proof. by rewrite mxsub_mul mxsub_id. Qed.
+
+Lemma mulmx_colsub m n n' p g (A : 'M_(m, p)) (B : 'M_(p, n)) :
+  A *m colsub g B = colsub g (A *m B) :> 'M_(m, n').
+Proof. by rewrite mxsub_mul mxsub_id. Qed.
+
 Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) :
   delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2).
 Proof.
@@ -1950,6 +2141,12 @@ rewrite -diag_const_mx mul_mx_diag.
 by apply/matrixP=> i j; rewrite !mxE mulr1.
 Qed.
 
+Lemma rowsubE m m' n f (A : 'M_(m, n)) :
+   rowsub f A = rowsub f 1%:M *m A :> 'M_(m', n).
+Proof. by rewrite mul_rowsub_mx mul1mx. Qed.
+
+(* mulmx and col_perm, row_perm, xcol, xrow *)
+
 Lemma mul_col_perm m n p s (A : 'M_(m, n)) (B : 'M_(n, p)) :
   col_perm s A *m B = A *m row_perm s^-1 B.
 Proof.
@@ -1985,6 +2182,12 @@ Proof. by rewrite /xcol col_permE tpermV. Qed.
 Lemma xrowE m n i1 i2 (A : 'M_(m, n)) : xrow i1 i2 A = tperm_mx i1 i2 *m A.
 Proof. exact: row_permE. Qed.
 
+Lemma perm_mxEsub n s : @perm_mx n s = rowsub s 1%:M.
+Proof. by rewrite /perm_mx row_permEsub. Qed.
+
+Lemma tperm_mxEsub n i1 i2 : @tperm_mx n i1 i2 = rowsub (tperm i1 i2) 1%:M.
+Proof. by rewrite /tperm_mx perm_mxEsub. Qed.
+
 Lemma tr_perm_mx n (s : 'S_n) : (perm_mx s)^T = perm_mx s^-1.
 Proof. by rewrite -[_^T]mulmx1 tr_row_perm mul_col_perm trmx1 mul1mx. Qed.
 
@@ -2106,6 +2309,14 @@ Proof.
 by move=> le_r_n; rewrite mulmxBl mul1mx mul_pid_mx_copid // oppr0 addr0.
 Qed.
 
+Lemma pid_mxErow m n (le_mn : m <= n) :
+  pid_mx m = rowsub (widen_ord le_mn) 1%:M.
+Proof. by apply/matrixP=> i j; rewrite !mxE -!val_eqE/= ltn_ord andbT. Qed.
+
+Lemma pid_mxEcol m n (le_mn : m <= n) :
+  pid_mx n = colsub (widen_ord le_mn) 1%:M.
+Proof. by apply/matrixP=> i j; rewrite !mxE -!val_eqE/= ltn_ord andbT. Qed.
+
 (* Block products; we cover all 1 x 2, 2 x 1, and 2 x 2 block products. *)
 Lemma mul_mx_row m n p1 p2 (A : 'M_(m, n)) (Bl : 'M_(n, p1)) (Br : 'M_(n, p2)) :
   A *m row_mx Bl Br = row_mx (A *m Bl) (A *m Br).
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index f1cc062..4c1d83e 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -366,6 +366,10 @@ Qed.
 Lemma col_leq_rank m n (A : 'M_(m, n)) : (n <= \rank A) = row_full A.
 Proof. by rewrite /row_full eqn_leq rank_leq_col. Qed.
 
+Lemma eq_row_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
+  (A :=: B)%MS -> row_full A = row_full B.
+Proof. by rewrite /row_full => ->. Qed.
+
 Let unitmx1F := @unitmx1 F.
 Lemma row_ebase_unit m n (A : 'M_(m, n)) : row_ebase A \in unitmx.
 Proof.
@@ -580,6 +584,10 @@ Proof.
 by case/submxP=> A' ->; case/submxP=> B' ->; rewrite -mulmxDl submxMl.
 Qed.
 
+Lemma rowsub_sub m1 m2 n (f : 'I_m2 -> 'I_m1) (A : 'M_(m1, n)) :
+  (rowsub f A <= A)%MS.
+Proof. by rewrite rowsubE mulmx_sub. Qed.
+
 Lemma summx_sub m1 m2 n (B : 'M_(m2, n))
                 I (r : seq I) (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.
@@ -592,10 +600,11 @@ Lemma scalemx_sub m1 m2 n a (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
 Proof. by case/submxP=> A' ->; rewrite scalemxAl submxMl. Qed.
 
 Lemma row_sub m n i (A : 'M_(m, n)) : (row i A <= A)%MS.
-Proof. by rewrite rowE submxMl. Qed.
+Proof. exact: rowsub_sub. Qed.
 
 Lemma eq_row_sub m n v (A : 'M_(m, n)) i : row i A = v -> (v <= A)%MS.
 Proof. by move <-; rewrite row_sub. Qed.
+Arguments eq_row_sub [m n v A].
 
 Lemma nz_row_sub m n (A : 'M_(m, n)) : (nz_row A <= A)%MS.
 Proof. by rewrite /nz_row; case: pickP => [i|] _; rewrite ?row_sub ?sub0mx. Qed.
@@ -933,6 +942,14 @@ Lemma eqmx_cast m1 m2 n (A : 'M_(m1, n)) e :
   ((castmx e A : 'M_(m2, n)) :=: A)%MS.
 Proof. by case: e A; case: m2 / => A e; rewrite castmx_id. Qed.
 
+Lemma row_full_castmx m1 m2 n (A : 'M_(m1, n)) e :
+  row_full (castmx e A  : 'M_(m2, n)) = row_full A.
+Proof. exact/eq_row_full/eqmx_cast. Qed.
+
+Lemma row_free_castmx m1 m2 n (A : 'M_(m1, n)) e :
+  row_free (castmx e A  : 'M_(m2, n)) = row_free A.
+Proof. by rewrite /row_free eqmx_cast; congr (_ == _); rewrite e.1. Qed.
+
 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.
 Proof.
@@ -947,6 +964,36 @@ case: (eqmx_conform <<A>>%MS A) => // eq_id_gen.
 exact: eqmx_trans (genmxE A).
 Qed.
 
+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.
+Proof. by rewrite rowsub_comp rowsubE mulmx_sub. Qed.
+
+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.
+Proof. by move=> /eq_rowsub->; rewrite rowsub_comp_sub. Qed.
+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.
+Proof.
+rewrite rowsub_comp rowsubE; apply: eqmxMfull.
+by rewrite -perm_mxEsub row_full_unit unitmx_perm.
+Qed.
+
+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.
+Proof.
+move=> leq_pn g_inj; have eq_np : n == p by rewrite eqn_leq leq_pn (inj_leq g).
+rewrite (eqP eq_np) in g g_inj *.
+rewrite (eq_rowsub (f \o (perm g_inj))); last by move=> i; rewrite /= permE.
+exact: eqmx_rowsub_comp_perm.
+Qed.
+
+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.
+Proof. by move=> leq_pn h_inj /eq_rowsub->; apply: eqmx_rowsub_comp. Qed.
+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)).
@@ -1234,6 +1281,26 @@ move=> Ainj; rewrite -kermx_eq0; apply/eqP/row_matrixP => i.
 by rewrite row0; apply/Ainj; rewrite -row_mul mulmx_ker row0.
 Qed.
 
+Lemma row_freePn m n (M : 'M[F]_(m, n)) :
+ reflect (exists i, (row i M <= row' i M)%MS) (~~ row_free M).
+Proof.
+rewrite -kermx_eq0; apply: (iffP (rowV0Pn _)) => [|[i0 /submxP[D rM]]].
+  move=> [v /sub_kermxP vM_eq0 /rV0Pn[i0 vi0_neq0]]; exists i0.
+  have := vM_eq0; rewrite mulmx_sum_row (bigD1_ord i0)//=.
+  move=> /(canRL (addrK _))/(canRL (scalerK _))->//.
+  rewrite sub0r scalerN -scaleNr scalemx_sub// summx_sub// => l _.
+  by rewrite scalemx_sub// -row_rowsub row_sub.
+exists (\row_j oapp (D 0) (- 1) (unlift i0 j)); last first.
+  by apply/rV0Pn; exists i0; rewrite !mxE unlift_none/= oppr_eq0 oner_eq0.
+apply/sub_kermxP; rewrite mulmx_sum_row (bigD1_ord i0)//= !mxE.
+rewrite unlift_none scaleN1r rM mulmx_sum_row addrC -sumrB big1 // => l _.
+by rewrite !mxE liftK row_rowsub subrr.
+Qed.
+
+Lemma negb_row_free m n (M : 'M[F]_(m, n)) :
+  ~~ row_free M = [exists i, (row i M <= row' i M)%MS].
+Proof. exact/row_freePn/existsP. Qed.
+
 Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
   A *m B = 0 -> \rank A + \rank B <= n.
 Proof.
@@ -2060,6 +2127,8 @@ Arguments mxdirect_sumsP {F I P n A_}.
 Arguments mxdirect_sumsE {F I P n S_}.
 Arguments eigenspaceP {F n g a m W}.
 Arguments eigenvalueP {F n g a}.
+Arguments submx_rowsub [F m1 m2 m3 n] h [f g A] _ : rename.
+Arguments eqmx_rowsub [F m1 m2 m3 n] h [f g A] _ : rename.
 
 Arguments mxrank {F m%N n%N} A%MS.
 Arguments complmx {F m%N n%N} A%MS.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index dca9a48..7d65f9e 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1281,6 +1281,9 @@ apply: (iffP eqP) => [eqfA |]; last exact: card_in_image.
 by apply/dinjectiveP; apply/card_uniqP; rewrite size_map -cardE.
 Qed.
 
+Lemma leq_card_in A : {in A &, injective f} -> #|A| <= #|T'|.
+Proof. by move=> /card_in_image <-; rewrite max_card. Qed.
+
 Hypothesis injf : injective f.
 
 Lemma card_image A : #|image f A| = #|A|.
@@ -1295,6 +1298,8 @@ rewrite -card_image /=; apply: eq_card => y.
 by rewrite [y \in _]image_pre !inE andbC.
 Qed.
 
+Lemma leq_card : #|T| <= #|T'|. Proof. exact: (leq_card_in (in2W _)). Qed.
+
 Hypothesis card_range : #|T| = #|T'|.
 
 Lemma inj_card_onto y : y \in codom f.
@@ -1308,6 +1313,8 @@ Qed.
 End CardFunImage.
 
 Arguments image_injP {T T' f A}.
+Arguments leq_card_in [T T'] f.
+Arguments leq_card [T T'] f.
 
 Section FinCancel.
 
@@ -1866,6 +1873,10 @@ Qed.
 Lemma rev_ord_inj {n} : injective (@rev_ord n).
 Proof. exact: inv_inj rev_ordK. Qed.
 
+Lemma inj_leq m n (f : 'I_m -> 'I_n) : injective f -> m <= n.
+Proof. by move=> /leq_card; rewrite !card_ord. Qed.
+Arguments inj_leq [m n] f _.
+
 (* bijection between any finType T and the Ordinal finType of its cardinal *)
 Section EnumRank.