proposition: Lemma ex_diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) -> {s | similar A (diag_mx_seq n.+1 n.+1 s)}.
proof: Proof. move=> H; exists (root_seq (char_poly A)). exact: diagonalization. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements) CoqEAL(frobenius_form)