English
The product over a sigma-type equals the iterated product: ∏ x, f x = ∏ x, ∏ y, f ⟨x,y⟩ when f: Sigma α → M.
Русский
Произведение над сигмонами равно повторному произведению: ∏ x, f x = ∏ x, ∏ y, f ⟨x,y⟩.
LaTeX
$$$\\prod_{x \\in \\Sigma}\\! f(x) = \\prod_{x} \\prod_{y} f\\langle x,y\\rangle$$$
Lean4
/-- Product over a sigma type equals the repeated product, curried version.
This version is useful to rewrite from right to left. -/
@[to_additive /-- Sum over a sigma type equals the repeated sum, curried version.
This version is useful to rewrite from right to left. -/
]
theorem prod_sigma' {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M]
(f : (i : ι) → α i → M) : ∏ x : Sigma α, f x.1 x.2 = ∏ x, ∏ y, f x y :=
prod_sigma ..
