proposition: Lemma diagonalizable_diag {n} (d : 'rV[F]_n) : diagonalizable (diag_mx d).
proof: Proof. exists 1%:M; rewrite ?unitmx1// /(diagonalizable_for _ _). by rewrite conj1mx diag_mx_is_diag. 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)