English
Let s,t be finite subsets of ι and f a function from ι to a commutative monoid M. Then the product over s equals the product over the intersection times the product over the elements of s not in t; i.e., (∏ x∈s∩t f(x)) · (∏ x∈s\\t f(x)) = ∏ x∈s f(x).
Русский
Пусть s,t — конечные подмножества множества ι, и функция f : ι → M, где M — коммутативная моноида. Тогда произведение по x из s равно произведению по x из s∩t умноженному на произведение по x из s\\t: (∏_{x∈s∩t} f(x)) · (∏_{x∈s\\t} f(x)) = ∏_{x∈s} f(x).
LaTeX
$$$\\left(\\prod_{x \\in s \\cap t} f(x)\\right) \\cdot \\left(\\prod_{x \\in s \\setminus t} f(x)\\right) = \\prod_{x \\in s} f(x)$$$
Lean4
@[to_additive]
theorem prod_inter_mul_prod_diff [DecidableEq ι] (s t : Finset ι) (f : ι → M) :
(∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x :=
by
convert (s.prod_piecewise t f f).symm
simp +unfoldPartialApp [Finset.piecewise]
