proposition: 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: 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.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)