proposition: Lemma det_Jordan_block (lam : R) n : \det (Jordan_block lam n) = lam ^+ n.
proof: Proof. rewrite det_triangular_mx; last by apply: upt_Jordan_block. rewrite -{8}[n]card_ord -prodr_const. by apply: eq_bigr=> 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)