diff options
| author | Cyril Cohen | 2020-09-03 12:59:09 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-08 02:11:28 +0200 |
| commit | 5d90649f226e80256ad903db9b8a0c21042f5a0a (patch) | |
| tree | 42b886e17478d4f94ff03eb83086996afbb10904 /mathcomp | |
| parent | c43abda6504f909db9884f2c42f764378471129f (diff) | |
Lemma mul_rvP
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index a7920ed..100eed7 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1678,6 +1678,9 @@ apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. +Lemma mul_rVP m n A B :((@mulmx 1 m n)^~ A =1 mulmx^~ B) <-> (A = B). +Proof. by split=> [eqAB|->//]; apply/row_matrixP => i; rewrite !rowE eqAB. Qed. + Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : row i (A *m B) = row i A *m B. Proof. by rewrite !rowE mulmxA. Qed. |