The colour character of a pair

The colour character is multiplicative in the colour vector: the character of a pair of colourings is the product of the two characters at the same permutation.

theorem RS.colourChar_mul {n k : ℕ} (α β : Fin k → ℕ) (π : Equiv.Perm (Fin n)) : colourChar α π * colourChar β π = {p : Fin n → Fin k × Fin k | (∀ (a : Fin k), fibreCard (fun (i : Fin n) => (p i).1) a = α a) ∧ (∀ (b : Fin k), fibreCard (fun (i : Fin n) => (p i).2) b = β b) ∧ p ∘ ⇑π = p}.card

The colour character is multiplicative: a product of two characters counts the fixed pair-colourings with the two prescribed margins.