English
For commutative monoids M,N, the product over a finite set s of pairs (f x, g x) equals the pair of the products: ∏ x∈s f x, ∏ x∈s g x = ∏ x∈s (f x, g x).
Русский
Пусть M,N — коммутативные моноиды; тогда произведение по s пар (f x, g x) равно паре произведений: (∏ f x, ∏ g x).
LaTeX
$$$$ \\left( \\prod_{x \\in s} f(x), \\; \\prod_{x \nobreakin s} g(x) \\right) = \\prod_{x \\in s} (f(x), g(x)). $$$$
Lean4
@[to_additive prod_mk_sum]
theorem prod_mk_prod [CommMonoid M] [CommMonoid N] (s : Finset ι) (f : ι → M) (g : ι → N) :
(∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) :=
haveI := Classical.decEq ι
Finset.induction_on s rfl (by simp +contextual [Prod.ext_iff])
