proposition: Lemma det_line_comb_eq : forall n k l a (M: 'M[R]_n), k == l -> \det (line_comb k l a M) = (1 + a) * \det M.
proof: Proof. move => n k l a M /eqP ->; clear k. have h : row l (line_comb l l a M) = 1 *: row l M + a *: row l M. - rewrite /line_scale. by apply/rowP => i; rewrite !mxE eqxx !mxE mul1r. rewrite (determinant_multilinear h) ?mulrDl //. rewrite /line_scale; apply/matrixP => i j; rewrite !mxE. by rewrite eq_sym (negbTE (neq_lift l i)) !mxE. rewrite /line_scale; apply/matrixP => i j; rewrite !mxE. by rewrite eq_sym (negbTE (neq_lift l i)) !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)