proposition: Lemma diagonalizable_forLR n {P : 'M[F]_n} {A} : P \in unitmx -> reflect (exists D, A = conjmx (invmx P) (diag_mx D)) (diagonalizable_for P A).
proof: Proof. by move=> Punit; apply: (iffP diagonalizable_forPex) => -[D /(simmxLR Punit)]; 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)