proposition: Lemma det_mlinear (n: nat) (f : 'I_n -> 'I_n -> R) (g : 'I_n -> R) : \det (\matrix_(i, j) (f i j * g j)) = \prod_(i < n) g i * \det (\matrix_(i, j) (f i j)).
proof: Proof. case: n => [|n] in f g *; first by rewrite big_ord0 mul1r !det_mx00. rewrite -det_tr (_ : _^T = \matrix_(j, i) (f i j * g j)); last first. by apply/matrixP => i j; rewrite !mxE. rewrite (@det_mlinear_rec _ _ _ n.+1) //; congr (_ * _). by under eq_bigr do rewrite inord_val. rewrite -det_tr; congr (\det _). by apply/matrixP => i j; rewrite !mxE ltnNge -ltnS ltn_ord /= mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2 mathcomp(finfield)