diff options
| author | Cyril Cohen | 2020-09-03 00:40:46 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-07 11:27:05 +0200 |
| commit | e7067ea1ea730fd4fd4d3daf556c6f712ffe04a8 (patch) | |
| tree | c1212b0ad263aaf172f36ffd6e0954bd11255d59 /mathcomp/algebra/matrix.v | |
| parent | 9adc523e89022fc6ac77471fb3fe381ad344d060 (diff) | |
Polynomial evaluation and minimal poly of a diagonal matrix
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1730b0b..823b08b 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2603,6 +2603,16 @@ Lemma det_lblock n1 n2 Aul (Adl : 'M[R]_(n2, n1)) Adr : \det (block_mx Aul 0 Adl Adr) = \det Aul * \det Adr. 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: n => [|n IHn] in A * => /is_trig_mxP Atrig; rewrite ?big_ord0 ?det_mx00//. +rewrite -[n.+1]/(1 + n)%N in A Atrig *; rewrite big_ord_recl -[A in LHS]submxK. +have -> : ursubmx A = 0 by apply/matrixP => i j; rewrite !mxE Atrig//= ord1. +rewrite det_lblock IHn; last by apply/is_trig_mxP => *; rewrite !mxE Atrig. +rewrite [ulsubmx A]mx11_scalar det_scalar1 !mxE !lshift0; congr (_ * _). +by apply: eq_bigr => i; rewrite !mxE !rshift1. +Qed. + End ComMatrix. Arguments lin_mul_row {R m n} u. |