sum_pow_eq_sum_piAntidiag — Mathlib

English

For Finset s in a commutative semiring and function f, the nth power of the sum equals the antidiagonal multinomial expansion with the appropriate product across s.

Русский

Для конечного множества s в коммутативной полупомещении и функции f, n-я степенная сумма распадается по антидиагонали с мультиномиалами и соответствующим произведением по s.

LaTeX

$$$\Big(\sum_{i\in s} f(i)\Big)^n = \sum_{k\in s.sym(n)} \mathrm{multinomial}(s,k) \; \prod_{i\in s} f(i)^{k(i)}$$$

Lean4

theorem sum_pow_eq_sum_piAntidiag (s : Finset α) (f : α → R) (n : ℕ) :
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ piAntidiag s n, multinomial s k * ∏ i ∈ s, f i ^ k i :=
  by
  simp_rw [← noncommProd_eq_prod]
  rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]

Похожие утверждения