proposition: Lemma det_mulmx n (A B : 'M[R]_n) : \det (A *m B) = \det A * \det B.
proof: Proof. rewrite big_distrl /=. pose F := ('I_n ^ n)%type; pose AB s i j := A i j * B j (s i). transitivity (\sum_(f : F) \sum_(s : 'S_n) (-1) ^+ s * \prod_i AB s i (f i)). rewrite exchange_big; apply: eq_bigr => /= s _; rewrite -big_distrr /=. congr (_ * _); rewrite -(bigA_distr_bigA (AB s)) /=. by apply: eq_bigr => x _; rewrite mxE. rewrite (bigID (fun f : F => injectiveb f)) /= addrC big1 ?add0r => [|f Uf]. rewrite (reindex (@pval _)) /=; last first. pose in_Sn := insubd (1%g : 'S_n). by exists in_Sn => /= f Uf; first apply: val_inj; apply: insubdK. apply: eq_big => /= [s | s _]; rewrite ?(valP s) // big_distrr /=. rewrite (reindex_inj (mulgI s)); apply: eq_bigr => t _ /=. rewrite big_split /= [in LHS]mulrA mulrCA mulrA mulrCA mulrA. rewrite -signr_addb odd_permM !pvalE; congr (_ * _); symmetry. by rewrite (reindex_perm s); apply: eq_bigr => i; rewrite permM. transitivity (\det (\matrix_(i, j) B (f i) j) * \prod_i A i (f i)). rewrite mulrC big_distrr /=; apply: eq_bigr => s _. rewrite mulrCA big_split //=; congr (_ * (_ * _)). by apply: eq_bigr => x _; rewrite mxE. case/injectivePn: Uf => i1 [i2 Di12 Ef12]. by rewrite (determinant_alternate Di12) ?simp //= => j; rewrite !mxE Ef12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)