proposition: Lemma det_mulmx : forall n (A B : 'M_n), \det (A *m B) === \det A * \det B.
proof: Proof. move=> n A B. pose AB (f : {ffun _}) := \matrix_(i, j) (A i (f i) * B (f i) j). transitivity (\sum_f \det (AB f)). rewrite{2}/determinant. setoid_rewrite (exchange_big (I:=finfun_of_finType (ordinal_finType n) (ordinal_finType n))). apply eq_bigr => /= s _. rewrite <- big_distrr => /=; apply rmul_morph; first by reflexivity. rewrite/mulmx. setoid_rewrite (bigA_distr_bigA (I:=ordinal_finType n)). by apply eq_bigr=>s' _; reflexivity. pose P_inj := fun f : {ffun 'I_n -> 'I_n} => injectiveb f. setoid_rewrite (bigID _ P_inj xpredT (fun f => \det (AB f)))=> /=. setoid_rewrite (big1 (I:=finfun_of_finType (ordinal_finType n) (ordinal_finType n))) at 2=>[|f]; last first. rewrite{}/P_inj; case/injectivePn=>i0;case=>j0 neq eq; rewrite{}/AB /determinant. setoid_rewrite big_split; setoid_rewrite rmul_comm at 2; setoid_rewrite rmul_assoc. rewrite <- big_distrl; rewrite -/(\det \matrix_(i,j) B (f i) j). by rewrite -> (alternate_determinant neq)=>[|i]; [ring|rewrite eq; reflexivity]. setoid_rewrite (reindex (J:=perm_for_finType (ordinal_finType n)) (h:=fun s => pval s)); last first. have s0 : 'S_n := 1%g; pose uf (f : {ffun 'I_n -> 'I_n}) := uniq (val f). exists (insubd s0) => /= f Uf; first apply: val_inj; exact: insubdK. setoid_rewrite (eq_bigl (I:=perm_for_finType (ordinal_finType n)) (P1:=fun j => P_inj (pval j)) (P2:=predT) _ (fun j => \det (AB (pval j)))); last by case. rewrite{2}/determinant=>{P_inj}; setoid_rewrite (big_distrl _ (\det _)). ring_simplify; apply eq_bigr=>s _; rewrite{}/AB (pvalE s) {2}/determinant. setoid_rewrite big_distrr. transitivity (\sum_(s' : 'S_n) (- (1)) ^+ s * (- rI) ^+ s' * (\prod_(i < n) A i (s i) * \prod_(i < n) B i (s' i))); last by apply eq_bigr=> j _; ring. have : forall s' : 'S_n, req ((- rI) ^+ s * (- rI) ^+ s') ((-rI) ^+ (s * s')%g). by move=>s'; rewrite odd_permM; case: (odd_perm s); case: (odd_perm s')=>/=; ring. move=>eq_puiss; setoid_rewrite eq_puiss; clear eq_puiss. setoid_rewrite (reindex (h:=fun t => (s^-1%g * t)%g)); last first. by exists [eta mulg s]=>s' _ /=; [apply (mulKVg s s') | apply (mulKg s s')]. apply eq_bigr=> s' _; rewrite (mulKVg s s'); apply rmul_morph; first by reflexivity. setoid_rewrite (reindex (h:=s)) at 3; last by exists (s^-1)%g=>i _; [rewrite permK|rewrite permKV]. setoid_rewrite big_split; apply rmul_morph; first by reflexivity. by apply eq_bigr=>i _; rewrite -permM (mulKVg s s'); reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms