English
For a finite set s and function f, the nth power of the sum equals the sum over the symmetric n-convolutions (piAntidiag) of multinomial coefficients times the products of f powers.
Русский
Для конечного множества s и функции f степень суммы распадается на сумму по симметрическим конволюциям n-мера мультиномиалов и произведения степеней f.
LaTeX
$$$\Big(\sum_{i\in s} f(i)\Big)^n = \sum_{k\in s.sym(n)} \mathrm{multinomial}(s,k) \; (f(i)^{k(i)})$$$
Lean4
/-- The **binomial theorem** -/
theorem add_pow [CommSemiring R] (x y : R) (n : ℕ) :
(x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m :=
(Commute.all x y).add_pow n
