proposition: Lemma detAB_weight : \det (A *m B) = \sum_(fz : Z) (weight fz.1 fz.2).
proof: Proof. rewrite /determinant /weight. rewrite (split_sumZ_sf _ xpredT) /=. apply/eq_big => // s _. rewrite -big_distrr /=; congr (_ * _). set F := fun n m => A n m * B m (s n). rewrite -(bigA_distr_bigA F) /=. apply/eq_big => // i _. by rewrite !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor