diff options
| author | Laurent Théry | 2020-09-28 08:41:58 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-28 08:41:58 +0200 |
| commit | a97b433c2d81c702fe690101a6e4e7afb4a3c28d (patch) | |
| tree | 23daffbce553ac1ddfdb22ee9e5d9d4c35937518 | |
| parent | 6d8f919bbc6a103378005d282fb6018bb63c5026 (diff) | |
| parent | 9eb54ad40f57b90d9c3b611a930994f99a46c7ea (diff) | |
Merge pull request #598 from CohenCyril/det_mx11
det_mx11
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 7 |
2 files changed, 7 insertions, 2 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 95c0d63..0a59193 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -136,6 +136,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of dual lattices. +- in `matrix.v` new lemma `det_mx11`. + ### 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 02097a4..70f28ec 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2666,6 +2666,9 @@ Proof. by rewrite -{1}(mulr1 a) -scale_scalar_mx detZ det1 mulr1. Qed. Lemma det_scalar1 a : \det (a%:M : 'M[R]_1) = a. Proof. exact: det_scalar. Qed. +Lemma det_mx11 (M : 'M[R]_1) : \det M = M 0 0. +Proof. by rewrite {1}[M]mx11_scalar det_scalar. Qed. + Lemma det_mulmx n (A B : 'M[R]_n) : \det (A *m B) = \det A * \det B. Proof. rewrite big_distrl /=. @@ -2820,8 +2823,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. Lemma det_trig n (A : 'M[R]_n) : is_trig_mx A -> \det A = \prod_(i < n) A i i. Proof. elim/trigsqmx_ind => [|k x c B Bt IHB]; first by rewrite ?big_ord0 ?det_mx00. -rewrite det_lblock big_ord_recl [x]mx11_scalar det_scalar IHB//; congr (_ * _). - by rewrite -[ord0](lshift0 _ 0) block_mxEul mxE. +rewrite det_lblock big_ord_recl det_mx11 IHB//; congr (_ * _). + by rewrite -[ord0](lshift0 _ 0) block_mxEul. by apply: eq_bigr => i; rewrite -!rshift1 block_mxEdr. Qed. |