diff options
| -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. |