Theorems · Theorem · combinatorics

Finset.sum_pow

∀ {α : Type u_1} {R : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring R] {s : Finset α} (x : α → R) (n : ℕ),
  s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).countPerms * (Multiset.map x ↑k).prod

Defined in

Mathlib.Data.Nat.Choose.Multinomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqCommSemiring