proposition: Lemma BareissE : forall n (M: 'M[R]_(1 + n)), (forall p (h h': p.+1 <= 1 + n), lreg (pminor h h' M)) -> Bareiss M = \det M.
proof: Proof. rewrite /Bareiss => n M h. have h1 : lreg (1: R) by apply/lreg1. have h2 : forall (k:nat) (f1 f2: 'I_k.+1 -> 'I_n.+1), 1 ^+ k %| minor f1 f2 M. - by move => k f1 f2; rewrite expr1n dvd1r. move: (Bareiss_recE h1 h2 h). by rewrite expr1n mul1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations