fact: Definition weight (f: {ffun 'I_k -> 'I_l}) (s : 'S_k) := ((-1) ^+ s) * \prod_(i : 'I_k) (A i (f i) * B (f i) (s i)).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor