Preparation for the cycle-sum identity

The Fubini exchange between permutations and their fixed colourings, and the congruence lemmas allowing transfer of the cycle-sum identity from realized power sums to arbitrary prospective ones.

theorem RS.newtonH_congr {t t' : ℕ → ℂ} (k : ℕ) : (∀ (c : ℕ), 1 ≤ c → c ≤ k → t c = t' c) → newtonH t k = newtonH t' k

newtonH only depends on the first k power sums.

theorem RS.cycleProd_congr {n : ℕ} {t t' : ℕ → ℂ} (π : Equiv.Perm (Fin n)) (h : ∀ (c : ℕ), 1 ≤ c → c ≤ n → t c = t' c) : cycleProd t π = cycleProd t' π

cycleProd only depends on the first n power sums.

theorem RS.sum_perm_fixed_weight {n N : ℕ} (w : (Fin n → Fin N) → ℂ) : ∑ π : Equiv.Perm (Fin n), ∑ f : { f : Fin n → Fin N // f ∘ ⇑π = f }, w ↑f = ∑ f : Fin n → Fin N, ↑{π : Equiv.Perm (Fin n) | f ∘ ⇑π = f}.card * w f

Fubini for fixed colourings: summing a colouring weight over all permutations and their fixed colourings counts each colouring once per stabilizing permutation.