prod_prod_type_right — Mathlib

English

The product over a product type equals the product of fiberwise products, with the order rearranged in a standard rightward fashion: ∏ x, f x = ∏ x, ∏ y, f(x,y).

Русский

Произведение по произведению равно произведению по его волокне справа: ∏ x, f x = ∏ x, ∏ y, f(x,y).

LaTeX

$$$ \\displaystyle \\prod x, f x = \\prod x, \\prod y, f(x,y). $$$

Lean4

@[to_additive Fintype.sum_prod_type_right]
theorem prod_prod_type_right [CommMonoid γ] (f : α₁ × α₂ → γ) : ∏ x, f x = ∏ y, ∏ x, f (x, y) :=
  Finset.prod_product_right ..

Похожие утверждения