4 files changed, 98 insertions, 12 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index f7d7730..77d2e4f 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2889,11 +2889,11 @@ Qed.
 Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A *m a%:M = a *: A.
 Proof. by rewrite scalar_mxC mul_scalar_mx. Qed.
 
-Lemma comm_mxC n a (A : 'M[R]_n) : comm_mx A a%:M.
+Lemma comm_mx_scalar n a (A : 'M[R]_n) : comm_mx A a%:M.
 Proof. by rewrite /comm_mx mul_mx_scalar mul_scalar_mx. Qed.
 
-Lemma commCmx n a (A : 'M[R]_n) : comm_mx a%:M A.
-Proof. exact/comm_mx_sym/comm_mxC. Qed.
+Lemma comm_scalar_mx n a (A : 'M[R]_n) : comm_mx a%:M A.
+Proof. exact/comm_mx_sym/comm_mx_scalar. Qed.
 
 Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B :
    \tr (A *m B) = \tr (B *m A).
@@ -3140,16 +3140,16 @@ End ComMatrix.
 
 Arguments lin_mul_row {R m n} u.
 Arguments lin_mulmx {R m n p} A.
-Arguments comm_mxC {R n}.
-Arguments commCmx {R n}.
+Arguments comm_mx_scalar {R n}.
+Arguments comm_scalar_mx {R n}.
 Arguments diag_mx_comm {R n}.
 
 Canonical matrix_finAlgType (R : finComRingType) n' :=
   [finAlgType R of 'M[R]_n'.+1].
 
-Hint Resolve comm_mxC commCmx : core.
+Hint Resolve comm_mx_scalar comm_scalar_mx : core.
 
-Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mxC)
+Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar)
   (at level 10, only parsing) : fun_scope.
 Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing).
 
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index e65bc3c..7899a62 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -47,6 +47,10 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix.
 (*                   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). *)
@@ -1766,6 +1770,87 @@ have injfU: \rank (U *m f) = \rank U by rewrite -defV eqrUV.
 by have [g injg defUg] := complete_unitmx injfU; exists g; rewrite -?defUg.
 Qed.
 
+(* 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)].
+Local Notation mxf := maxrankfun.
+
+Lemma maxrowsub_free : row_free (rowsub mxf A).
+Proof.
+rewrite /mxf; case: arg_maxnP => //= f _ fM; apply/negP => /negP rfA.
+have [i NriA] : exists i, ~~ (row i A <= rowsub f A)%MS.
+  by apply/row_subPn; apply: contraNN rfA => /mxrankS; rewrite row_leq_rank.
+have [j rjfA] : exists j, (row (f j) A <= rowsub (f \o lift j) A)%MS.
+  case/row_freePn: rfA => j.
+  by rewrite row_rowsub row'Esub -mxsub_comp; exists j.
+pose g : 'I_m ^ \rank A := finfun [eta f with j |-> i].
+suff: (rowsub f A < rowsub g A)%MS by rewrite ltmxErank andbC ltnNge fM.
+rewrite ltmxE; apply/andP; split; last first.
+  apply: contra NriA; apply: submx_trans.
+  by rewrite (eq_row_sub j)// row_rowsub ffunE/= eqxx.
+apply/row_subP => k; rewrite !row_rowsub.
+have [->|/negPf eq_kjF] := eqVneq k j; last first.
+  by rewrite (eq_row_sub k)// row_rowsub ffunE/= eq_kjF.
+rewrite (submx_trans rjfA)// (submx_rowsub (lift j))// => l /=.
+by rewrite ffunE/= eq_sym (negPf (neq_lift _ _)).
+Qed.
+
+Lemma eq_maxrowsub : (rowsub mxf A :=: A)%MS.
+Proof.
+apply/eqmxP; rewrite -(eq_leqif (mxrank_leqif_eq _))//.
+  exact: maxrowsub_free.
+apply/row_subP => i; apply/submxP; exists (delta_mx 0 (mxf i)).
+by rewrite -rowE; apply/rowP => j; rewrite !mxE.
+Qed.
+
+Lemma maxrankfun_inj : injective mxf.
+Proof.
+move=> i j eqAij; have /row_free_inj := maxrowsub_free.
+move=> /(_ 1%N) /(_ (delta_mx 0 i) (delta_mx 0 j)).
+rewrite -!rowE !row_rowsub eqAij => /(_ erefl) /matrixP /(_ 0 i) /eqP.
+by rewrite !mxE eqxx/=; case: (i =P j); rewrite // oner_eq0.
+Qed.
+
+Variable (rkA : row_full A).
+
+Lemma maxrowsub_full : row_full (rowsub mxf A).
+Proof. by rewrite /row_full eq_maxrowsub. Qed.
+Hint Resolve maxrowsub_full : core.
+
+Definition fullrankfun : 'I_m ^ n := finfun (mxf \o cast_ord (esym (eqP rkA))).
+Local Notation frf := fullrankfun.
+
+Lemma fullrowsub_full : row_full (rowsub frf A).
+Proof.
+by rewrite mxsub_ffunl rowsub_comp rowsub_cast esymK row_full_castmx.
+Qed.
+
+Lemma fullrowsub_unit : rowsub frf A \in unitmx.
+Proof. by rewrite -row_full_unit fullrowsub_full. Qed.
+
+Lemma fullrowsub_free : row_free (rowsub frf A).
+Proof.  by rewrite row_free_unit fullrowsub_unit. Qed.
+
+Lemma mxrank_fullrowsub : \rank (rowsub frf A) = n.
+Proof. exact/eqP/fullrowsub_full. Qed.
+
+Lemma eq_fullrowsub : (rowsub frf A :=: A)%MS.
+Proof.
+rewrite mxsub_ffunl rowsub_comp rowsub_cast esymK.
+exact: (eqmx_trans (eqmx_cast _ _) eq_maxrowsub).
+Qed.
+
+Lemma fullrankfun_inj : injective frf.
+Proof.
+by move=> i j; rewrite !ffunE => /maxrankfun_inj /(congr1 val)/= /val_inj.
+Qed.
+
+End MaxRankSubMatrix.
+
 Section SumExpr.
 
 (* This is the infrastructure to support the mxdirect predicate. We use a     *)
@@ -2291,7 +2376,7 @@ Lemma comm_mx_stable_eigenspace (f g : 'M[F]_n) a :
   comm_mx f g -> stablemx (eigenspace f a) g.
 Proof.
 move=> cfg; rewrite comm_mx_stable_ker//.
-by apply/comm_mx_sym/comm_mxB => //; apply:comm_mxC.
+by apply/comm_mx_sym/comm_mxB => //; apply:comm_mx_scalar.
 Qed.
 
 End Commutation.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index c7f8fb1..19a23e6 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -274,7 +274,7 @@ Section OneMatrix.
 
 Variable A : 'M[R]_n.
 
-Definition horner_mx := horner_morph (comm_mxC^~ A).
+Definition horner_mx := horner_morph (comm_mx_scalar^~ A).
 Canonical horner_mx_additive := [additive of horner_mx].
 Canonical horner_mx_rmorphism := [rmorphism of horner_mx].
 
@@ -317,7 +317,8 @@ Qed.
 
 Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p).
 Proof.
-by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx.
+move=> fg; apply: commr_horner => // i.
+by rewrite coef_map; apply/comm_scalar_mx.
 Qed.
 
 Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index fc24a4b..7da7ebc 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1584,7 +1584,7 @@ Arguments ltr01 {R}.
 Arguments normr_idP {R x}.
 Arguments normr0P {R V v}.
 Hint Resolve ler01 ltr01 ltr0Sn ler0n : core.
-Hint Extern 0 (is_true (0 <= norm _)) => exact: normr_ge0 : core.
+Hint Extern 0 (is_true (0 <= norm _)) => apply: normr_ge0 : core.
 
 Section NumDomainOperationTheory.
 
@@ -2977,7 +2977,7 @@ Definition lter_nnormr := (ler_nnorml, ltr_nnorml).
 
 End NormedZmoduleTheory.
 
-Hint Extern 0 (is_true (norm _ \is real)) => exact: normr_real : core.
+Hint Extern 0 (is_true (norm _ \is real)) => apply: normr_real : core.
 
 Lemma real_ler_norml x y : x \is real -> (`|x| <= y) = (- y <= x <= y).
 Proof.