proposition: Lemma BinetCauchy: \det (A *m B) = \sum_(f : {ffun 'I_k -> 'I_l} | strictf f) (minor id f A * minor f id B).
proof: Proof. pose cond := fun fz : Z => injectiveb fz.1. pose ffstrictf := fun (f: {ffun 'I_k -> 'I_l}) => strictf f. rewrite detAB_weight (bigID cond) /= sum_bad addr0. rewrite -gather_by_strictness (partition_big strict_from_f ffstrictf) /=. - apply/eq_big => // g hg. apply/congr_big => //. case => f pi; rewrite /cond /good /=. apply/andP/andP; case => /injectiveP h1. + rewrite /strict_from_f /=. case: injectiveP => [hinj | []] //. move/eqP => heq; split => //. case: (strict_fromP hinj) => hlt hrt. apply/forallP => x. by rewrite -heq (hrt x). move/forallP => hsame. have hcodom : forall x, (x \in codom f) = (x \in codom g) by move => x; rewrite (eqP (hsame x)). split; first by apply/injectiveP. case: (@strict_from_fP (f,pi) h1) => hstrict hcodom2. rewrite (strictf_uniq hstrict hg) // => x. by rewrite -hcodom2 hcodom. move => fz /injectiveP hf. by case: (strict_from_fP hf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor