English
An uncurried version of the previous fiberwise product identity: for f: α1 → α2 → γ, the product over x : α1 × α2 of f x.1 x.2 equals the product over y of the product over x of f x y.
Русский
Некуррированный аналог предыдущей формулы: для f: α1 → α2 → γ произведение по x : α1 × α2 от f x.1 x.2 равно произведению по y от произведения по x от f x y.
LaTeX
$$$ \\displaystyle \\prod x : \\alpha_1 \\times \\alpha_2, f x.1 x.2 = \\prod x : \\alpha_1, \\prod y : \\alpha_2, f x y.$$$
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.1 x.2 = ∏ x, ∏ y, f x y :=
Finset.prod_product' ..
