proposition: Lemma diagonalizableP n' (n := n'.+1) (A : 'M[F]_n) : diagonalizable A <-> exists2 rs, uniq rs & mxminpoly A %| \prod_(x <- rs) ('X - x%:P).
proof: Proof. split=> [[P Punit /diagonalizable_forPex[d /(simmxLR Punit)->]]|]. rewrite mxminpoly_uconj ?unitmx_inv// mxminpoly_diag. by eexists; [|by []]; rewrite undup_uniq. rewrite diagonalizablePeigen => -[rs rsu rsP]; exists rs => //. rewrite (big_nth 0) [X in (X :=: _)%MS](big_nth 0) !big_mkord in rsP *. rewrite (eq_bigr _ (fun _ _ => eigenspace_poly _ _)). apply: (eqmx_trans (eqmx_sym (kermxpoly_prod _ _)) (kermxpoly_min _)) => //. by move=> i j _ _; rewrite coprimep_XsubC root_XsubC nth_uniq. 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)