proposition: Lemma diagonalizable_conj_diag m n (V : 'M[F]_(m, n)) (d : 'rV[F]_n) : stablemx V (diag_mx d) -> row_free V -> diagonalizable (conjmx V (diag_mx d)).
proof: Proof. case: m n => [|m] [|n] in V d * => Vd rdV; rewrite ?thinmx0//=. by rewrite /row_free mxrank.unlock in rdV. apply/diagonalizableP; pose u := undup [seq d 0 i | i <- enum 'I_n.+1]. exists u; first by rewrite undup_uniq. by rewrite (dvdp_trans (mxminpoly_conj (f:=diag_mx d) _ _))// mxminpoly_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)