Coefficient of a product of complete homogeneous polynomials

The coefficient of a monomial w in the product ∏ i, hSub univ (c i) counts the number of tuples of symmetric-function indices whose combined weight equals w.

theorem RS.coeff_hSub_prod {k : ℕ} (c : Fin k → ℕ) (w : Fin k →₀ ℕ) : (∏ i : Fin k, hSub Finset.univ (c i)).coeff w = ↑(Fintype.card { W : (i : Fin k) → Sym (Fin k) (c i) // ∀ (j : Fin k), ∑ i : Fin k, Multiset.count j ↑(W i) = w j })

A coefficient of a product of complete homogeneous polynomials counts the tuples of multisets with the prescribed column sums.