prod_add_one — Mathlib

English

If R is a commutative semiring and s is finite, then the product over i∈s of (f(i) + 1) equals the sum over t∈powerset(s) of the product over i∈t of f(i).

Русский

Для коммутативной полугруппы (полугруппы без единицы?) и конечного множества s имеем аналогичное разложение.

LaTeX

$$$\\prod_{i\\in s} (f(i) + 1) = \\sum_{t\\in s.powerset} \\prod_{i\\in t} f(i)$$$

Lean4

theorem prod_add_one {f : ι → R} (s : Finset ι) : ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i := by
  classical simp only [prod_add, prod_const_one, mul_one]

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