prod_prod_type_right' — Mathlib

English

An uncurried variant of the fiberwise product identity: for f : α1 → α2 → γ, ∏ x : α1 × α2, f x.1 x.2 = ∏ y, ∏ x, 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 y, \\prod x, f x y.$$$

Lean4

/-- An uncurried version of `Finset.prod_prod_type_right`. -/
@[to_additive Fintype.sum_prod_type_right' /-- An uncurried version of `Finset.sum_prod_type_right` -/
    ]
theorem prod_prod_type_right' [CommMonoid γ] (f : α₁ → α₂ → γ) : ∏ x : α₁ × α₂, f x.1 x.2 = ∏ y, ∏ x, f x y :=
  Finset.prod_product_right' ..

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