diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 40 |
3 files changed, 54 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20809f3..ce197ca 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -84,6 +84,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `matrix.v` new lemmas about `map_mx`: `map_mx_id`, `map_mx_comp`, `eq_in_map_mx`, `eq_map_mx` and `map_mx_id_in`. +- in `matrix.v` new lemma `det_trig` + +- in `mxpoly.v` new lemmas `horner_mx_diag`, `char_poly_trig`, + `root_mxminpoly`, and `mxminpoly_diag` + ### 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 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. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index f33e291..9d54f35 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -297,6 +297,18 @@ Qed. End HornerMx. +Lemma horner_mx_diag (R : comRingType) (n' : nat) + (d : 'rV[R]_n'.+1) (p : {poly R}) : + horner_mx (diag_mx d) p = diag_mx (map_mx (horner p) d). +Proof. +apply/matrixP => i j; rewrite !mxE. +elim/poly_ind: p => [|p c ihp]; first by rewrite rmorph0 horner0 mxE mul0rn. +rewrite !hornerE mulrnDl rmorphD rmorphM /= horner_mx_X horner_mx_C !mxE. +rewrite (bigD1 j)//= ihp mxE ?eqxx mulr1n -mulrnAl big1 ?addr0//. + by case: (altP (i =P j)) => [->|]; rewrite /= !(mulr1n, addr0, mul0r). +by move=> k /negPf nkF; rewrite mxE nkF mulr0. +Qed. + Prenex Implicits horner_mx powers_mx. Section CharPoly. @@ -434,6 +446,14 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)). by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn). Qed. +Lemma char_poly_trig {R : comRingType} n (A : 'M[R]_n) : is_trig_mx A -> + char_poly A = \prod_(i < n) ('X - (A i i)%:P). +Proof. +move=> /is_trig_mxP Atrig; rewrite /char_poly det_trig. + by apply: eq_bigr => i; rewrite !mxE eqxx. +by apply/is_trig_mxP => i j lt_ij; rewrite !mxE -val_eqE ltn_eqF ?Atrig ?subrr. +Qed. + Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) := \matrix_(i < d, j < d) if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R. @@ -643,13 +663,31 @@ rewrite !hornerE rmorphD rmorphM /= horner_mx_X horner_mx_C scalerDl. by rewrite -scalerA mulmxDr mul_mx_scalar mulmxA -IHp -scalemxAl Av_av. Qed. +Lemma root_mxminpoly a : root p_A a = root (char_poly A) a. +Proof. by rewrite -eigenvalue_root_min eigenvalue_root_char. Qed. + End MinPoly. +Lemma mxminpoly_diag {F : fieldType} {n} (d : 'rV[F]_n.+1) + (u := undup [seq d 0 i | i <- enum 'I_n.+1]) : + mxminpoly (diag_mx d) = \prod_(r <- u) ('X - r%:P). +Proof. +apply/eqP; rewrite -eqp_monic ?mxminpoly_monic ?monic_prod_XsubC// /eqp. +rewrite mxminpoly_min/=; last first. + rewrite horner_mx_diag; apply/matrixP => i j; rewrite !mxE horner_prod. + case: (altP (i =P j)) => [->|neq_ij//]; rewrite mulr1n. + rewrite (bigD1_seq (d 0 j)) ?undup_uniq ?mem_undup ?map_f// /=. + by rewrite hornerD hornerN hornerX hornerC subrr mul0r. +apply: uniq_roots_dvdp; last by rewrite uniq_rootsE undup_uniq. +apply/allP => x; rewrite mem_undup root_mxminpoly char_poly_trig//. +rewrite -(big_map _ predT (fun x => _ - x%:P)) root_prod_XsubC. +by move=> /mapP[i _ ->]; apply/mapP; exists i; rewrite ?(mxE, eqxx). +Qed. Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner. Arguments mx_inv_hornerK {F n' A} [B] AnB. Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename. - + (* Parametricity. *) Section MapRingMatrix. |