Coefficient of a power of p₁

The coefficient of a monomial w in (∑ l, X l) ^ |T| counts the number of functions T → Fin k whose fibre sizes match w.

theorem RS.coeff_p1_pow {k : ℕ} (T : Type) [Fintype T] (w : Fin k →₀ ℕ) : ((∑ l : Fin k, MvPolynomial.X l) ^ Fintype.card T).coeff w = ↑{t : T → Fin k | ∀ (a : Fin k), {i : T | t i = a}.card = w a}.card

A coefficient of a power of the first power sum counts the functions with the prescribed fibre sizes.