English
For a finite set s and functions f,g: ι → R with R a commutative ring, the product of (f(i) − g(i)) over i∈s equals the sum over t⊆s of (−1)^{|t|} times the product over i∈s\\t f(i) times the product over i∈t g(i).
Русский
Для конечного множества s и функций f,g: ι → R, произведение (f(i)−g(i)) по i∈s равно сумме по подмножествам t⊆s (−1)^{|t|} умножить на произведение i∈s\\t f(i) и произведение i∈t g(i).
LaTeX
$$$\\prod_{i\\in s} (f(i) - g(i)) = \\sum_{t\\in s.powerset} (-1)^{|t|} \\left( \\prod_{i\\in s\\setminus t} f(i) \\right) \\left( \\prod_{i\\in t} g(i) \\right)$$$
Lean4
/-- The product of `f i - g i` over all of `s` is the sum over the powerset of `s` of the product of
`g` over a subset `t` times the product of `f` over the complement of `t` times `(-1) ^ #t`. -/
theorem prod_sub [DecidableEq ι] (f g : ι → R) (s : Finset ι) :
∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, (-1) ^ #t * (∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i := by
simp [sub_eq_neg_add, prod_add, prod_neg, mul_right_comm]
