Merge pull request #597 from CohenCyril/inj_row_free

Injectivity for additive functions and mulmxr.

2 files changed, 17 insertions, 4 deletions

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 686da21..f1cc062 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -686,6 +686,11 @@ case/row_freeP=> A' AK; apply: can_inj (mulmx^~ A') _ => B.
 by rewrite -mulmxA AK mulmx1.
 Qed.
 
+(* 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).
 Proof.
 apply/row_fullP/idP=> [[A'] | uA]; first by case/mulmx1_unit.
@@ -1222,6 +1227,13 @@ Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
   row_free B -> (A *m B == 0) = (A == 0).
 Proof. by rewrite -sub_kermx -kermx_eq0 => /eqP->; rewrite submx0. Qed.
 
+Lemma inj_row_free m n (A : 'M_(m, n)) :
+  (forall v : 'rV_m, v *m A = 0 -> v = 0) -> row_free A.
+Proof.
+move=> Ainj; rewrite -kermx_eq0; apply/eqP/row_matrixP => i.
+by rewrite row0; apply/Ainj; rewrite -row_mul mulmx_ker row0.
+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.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 9a3c7d7..6128fa0 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1878,6 +1878,9 @@ Proof. by rewrite -[0]subr0 raddfB subrr. Qed.
 Lemma raddf_eq0 x : injective f -> (f x == 0) = (x == 0).
 Proof. by move=> /inj_eq <-; rewrite raddf0. Qed.
 
+Lemma raddf_inj : (forall x, f x = 0 -> x = 0) -> injective f.
+Proof. by move=> fI x y eqxy; apply/subr0_eq/fI; rewrite raddfB eqxy subrr. Qed.
+
 Lemma raddfN : {morph f : x / - x}.
 Proof. by move=> x /=; rewrite -sub0r raddfB raddf0 sub0r. Qed.
 
@@ -4933,10 +4936,7 @@ by rewrite -rmorphM mulVf // mulr0 rmorph1 ?oner_eq0.
 Qed.
 
 Lemma fmorph_inj : injective f.
-Proof.
-move=> x y eqfxy; apply/eqP; rewrite -subr_eq0 -fmorph_eq0 rmorphB //.
-by rewrite eqfxy subrr.
-Qed.
+Proof. by apply/raddf_inj => x /eqP; rewrite fmorph_eq0 => /eqP. Qed.
 
 Lemma fmorph_eq1 x : (f x == 1) = (x == 1).
 Proof. by rewrite -(inj_eq fmorph_inj) rmorph1. Qed.
@@ -5899,6 +5899,7 @@ Definition size_sol := size_sol.
 Definition solve_monicpoly := solve_monicpoly.
 Definition raddf0 := raddf0.
 Definition raddf_eq0 := raddf_eq0.
+Definition raddf_inj := raddf_inj.
 Definition raddfN := raddfN.
 Definition raddfD := raddfD.
 Definition raddfB := raddfB.