diff options
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 12 |
1 files changed, 12 insertions, 0 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. |