diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 9 |
3 files changed, 24 insertions, 4 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 439515b..4182d48 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -137,6 +137,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). dual lattices. - in `matrix.v` new lemma `det_mx11`. +- in `ssralg.v`, new lemma `raddf_inj`, characterizing injectivity for + additive maps. +- in `mxalgebra.v`, new lemma `row_free_injr` which duplicates + `row_free_inj` but exposing `mulmxr` for compositionality purposes + (e.g. with `raddf_eq0`), and lemma `inj_row_free` characterizing + `row_free` matrices `A` through `v *m A = 0 -> v = 0` for all `v`. + ### Changed 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. |