Polynomial evaluation and minimal poly of a diagonal matrix

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.