proposition: Lemma char_poly_altE : forall n (M: 'M[R]_(1 + n)), char_poly_alt M = char_poly M.
proof: Proof. rewrite /char_poly_alt /char_poly => n M. by rewrite bareissE // => p h h'; exact/monic_lreg/pminor_char_poly_mx_monic. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(ssrcomplements minor dvdring) polydvd