proposition: Lemma det_lines_scale m a (M: 'M[R]_m) s: \det (foldl (fun N i => line_scale i a N) M s) = a ^+ (size s) * \det M.
proof: Proof. elim : s M => [ | hd tl hi] M //=. - by rewrite expr0 mul1r. by rewrite hi det_line_scale mulrA exprSr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)