proposition: Lemma det_line_comb : forall n k l a (M: 'M[R]_n), k != l -> \det (line_comb k l a M) = \det M.
proof: Proof. move => n k l a M hkl. have h : row k (line_comb k l a M) = 1 *: row k M + a *: row k (\matrix_(i < n) if i == k then row l M else row i M). by rewrite scale1r; apply/rowP => i; rewrite !mxE eqxx !mxE. rewrite (determinant_multilinear h). - rewrite mul1r [X in a * X](determinant_alternate hkl). + by rewrite mulr0 addr0. by move => x; rewrite !mxE eqxx eq_sym (negbTE hkl). - by apply/matrixP => i j; rewrite !mxE eq_sym (negbTE (neq_lift k i)) !mxE. by apply/matrixP => i j; rewrite !mxE eq_sym (negbTE (neq_lift k i)) !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)