Theorems · Theorem · combinatorics

Finset.sum_pow_of_commute

∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : Semiring R] (x : α → R) (s : Finset α)
  (hc : (↑s).Pairwise (Function.onFun Commute x)) (n : ℕ),
  s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

The multinomial theorem.

Defined in

Mathlib.Data.Nat.Choose.Multinomial

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqSemiring