proposition: Lemma char_poly_Jordan_block (lam : R) n : char_poly (Jordan_block lam n) = ('X - lam%:P) ^+n.
proof: Proof. rewrite char_poly_triangular_mx; last by apply: upt_Jordan_block. rewrite (eq_bigr (fun _ => ('X - lam%:P))) ?prodr_const ?card_ord //. by move=> i; rewrite mxE eqxx eqn_leq ltnn addr0. 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)