English
Let γ be a commutative monoid and f: α1 × α2 → γ. Then the product over x ∈ α1 × α2 of f x equals the product over a1 ∈ α1 of the product over a2 ∈ α2 of f(a1, a2).
Русский
Пусть γ — коммутативный моноид и f: α1 × α2 → γ. Тогда произведение по x ∈ α1 × α2 от f x равно произведению по a1 ∈ α1 от произведения по a2 ∈ α2 от f(a1, a2).
LaTeX
$$$ \\displaystyle \\prod x, f x = \\left( \\prod a_1, f(a_1, -) \\right) \\left( \\prod a_2, f(-, a_2) \\right) $$$
Lean4
/-- The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Fintype.prod_prod_type'`. -/
@[to_additive Fintype.sum_prod_type /-- The sum over a product type equals the sum of fiberwise
sums. For rewriting in the reverse direction, use `Fintype.sum_prod_type'`. -/
]
theorem prod_prod_type [CommMonoid γ] (f : α₁ × α₂ → γ) : ∏ x, f x = ∏ x, ∏ y, f (x, y) :=
Finset.prod_product ..
