proposition: Lemma diagonalizable_for_mxminpoly {n} {P A : 'M[F]_n.+1} (rs := undup [seq conjmx P A i i | i <- enum 'I_n.+1]) : P \in unitmx -> diagonalizable_for P A -> mxminpoly A = \prod_(r <- rs) ('X - r%:P).
proof: Proof. rewrite /rs => pu /(diagonalizable_forLR pu)[d {A rs}->]. rewrite mxminpoly_uconj ?unitmx_inv// mxminpoly_diag. by rewrite [in X in _ = X](@eq_map _ _ _ (d 0))// => i; rewrite conjmxVK// 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)