proposition: Lemma det_line_scale_mx : forall n k a (M: 'M[R]_n), \det (line_scale_mx k a M) = a * \det M.
proof: Proof. rewrite /line_scale_mx => n k a M. rewrite det_mulmx det_diag (bigD1 k) //= big1 /=; first by rewrite !mxE mulr1 eqxx. by move => i /negbTE h; rewrite !mxE h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly mxpoly)