sum_pow_mul_eq_add_pow — Mathlib

English

If s is finite with a linear order and f,g: ι → R, then the product over i∈s of (f(i) − g(i)) equals the product over i∈s f(i) minus a sum over i∈s of g(i) times the product over j<i of (f(j) − g(j)) times the product over j>i of f(j).

Русский

Если s конечно и упорядочено, то произведение (f(i)−g(i)) по i∈s равно произведению f(i) по i∈s минус сумма по i∈s от g(i) на произведение по j<i (f(j)−g(j)) и произведение по j>i f(j).

LaTeX

$$$\\prod_{i\\in s} (f(i) - g(i)) = \\left( \\prod_{i\\in s} f(i) \\right) - \\sum_{i\\in s} g(i) \\left( \\prod_{j\\in s, j

Lean4

/-- Summing `a ^ #t * b ^ (n - #t)` over all finite subsets `t` of a finset `s`
gives `(a + b) ^ #s`. -/
theorem sum_pow_mul_eq_add_pow (a b : R) (s : Finset ι) : (∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t)) = (a + b) ^ #s :=
  by
  classical
  rw [← prod_const, prod_add]
  refine Finset.sum_congr rfl fun t ht => ?_
  rw [prod_const, prod_const, ← card_sdiff_of_subset (mem_powerset.1 ht)]

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