sum_pow' — Mathlib

English

For any finite set s and function f, the n-th power of the sum over s of f equals the sum over p in piFinset of the product over i of f(p(i)).

Русский

Для конечного множества s и функции f равенство: (∑_{i∈s} f(i))^n = ∑_{p∈piFinset} ∏_{i} f(p(i)).

LaTeX

$$$\\left(\\sum_{a\\in s} f(a)\\right)^{n} = \\sum_{p\\in \\mathrm{piFinset}\\,\\dots} \\prod_{i} f(p(i))$$$

Lean4

theorem sum_pow' (s : Finset κ) (f : κ → R) (n : ℕ) :
    (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by
  convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp

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