proposition: Lemma bdetE : forall n (M : 'M[R]_(1 + n)), bdet M = \det M.
proof: Proof. move=> n M. rewrite /bdet char_poly_altE char_poly_det. have -> : - M = -1 *: M by apply/matrixP => i j; rewrite !mxE mulN1r. by rewrite 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(ssrcomplements minor dvdring) polydvd