proposition: Lemma step_weight (g f: {ffun 'I_k -> 'I_l}) (pi: 'S_k) (hf : injective f) (phi : 'S_k) : (forall x, f x = g (phi x)) -> let: sigma := (phi^-1 * pi)%g in weight f pi = ((-1)^+ phi * \prod_i (A i (g (phi i)))) * ((-1)^+ sigma * \prod_i (B (g i) (sigma i))).
proof: Proof. move => heq. rewrite mulrAC mulrA -signr_addb -odd_permM mulgA mulgV mul1g -mulrA. rewrite /weight big_split /=. congr (_ * _); rewrite mulrC. congr (_ * _); last first. - apply/eq_big => // i _. by rewrite heq. have hinf : injective phi by apply: perm_inj. rewrite [X in _ = X](reindex_inj hinf) /=. apply/eq_big => // i _. by rewrite -permM mulgA mulgV mul1g heq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor