diff options
| author | affeldt-aist | 2020-09-08 15:08:07 +0900 |
|---|---|---|
| committer | GitHub | 2020-09-08 15:08:07 +0900 |
| commit | e92551cb84089049902f8107c776b2ed5d935c92 (patch) | |
| tree | 96f98a38009ca4f489b88c050b32f28b756b66ba | |
| parent | b0697693bda2a4c49a38e9265abcf68613801210 (diff) | |
| parent | 5d90649f226e80256ad903db9b8a0c21042f5a0a (diff) | |
Merge pull request #577 from CohenCyril/mulmxP
Lemma mul_rVP
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1a5936f..ea71537 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -89,6 +89,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `index_ltn`, `in_take`, `in_take_leq`, `split_find_nth`, `split_find` and `nth_rcons_cat_find`. +- in `matrix.v` new lemma `mul_rVP`. + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 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. |