proposition: Lemma bdetE n (M : 'M[R]_(1 + n)) : bdet (polyR:= {poly R}) (@char_poly_mx R) head M = \det M.
proof: Proof. rewrite /bdet /head bareiss_char_polyE char_poly_det. have -> : (-M)%C = -M by []. by rewrite -scaleN1r detZ mulrA -expr2 sqrr_sign mul1r. 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)