proposition: Lemma Jordan_char_poly n (A : 'M_n.+1) : char_poly A = \prod_i ('X - ((Jordan_form A) i i)%:P).
proof: Proof. rewrite (similar_char_poly (Jordan A)). exact: (char_poly_triangular_mx (upt_Jordan A)). 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)