proposition: Lemma diagonalizable_forPex {m} {n} {P : 'M[F]_(m, n)} {A} : reflect (exists D, A ~_P (diag_mx D)) (diagonalizable_for P A).
proof: Proof. by apply: (iffP (diag_mxP _)) => -[D]/eqP; exists D. 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)