sum_pow — Mathlib

English

A variant of the binomial theorem in the Fintype setting: summing over all subsets of a finite type ι, a^{|s|} b^{|ι|-|s|} equals (a+b)^{|ι|}. The result is encoded via sum_pow_mul_eq_add_pow.

Русский

Вариант биномиальной теоремы в конечном типе: сумма по всем подмножествам ι от a^{|s|} b^{|ι|-|s|} равна (a+b)^{|ι|}.

LaTeX

$$$\\sum_{s\\subseteq \\iota} a^{|s|} b^{|\\iota|-|s|} = (a+b)^{|\\iota|}$$$

Lean4

theorem sum_pow (f : ι → R) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i) := by simp [sum_pow']

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