proposition: Lemma bareiss_char_polyE n (M : 'M[R]_(1 + n)) : bareiss_char_poly (@char_poly_mx R) M = char_poly M.
proof: Proof. rewrite /bareiss_char_poly bareissE // => p h h'. exact: 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(minor hrel param refinements seqmx)