English
Let R be a setoid on ι. The product over s of f equals the product over quotient representatives of the inner products of fibers, i.e., the same as in the previous partition formula.
Русский
Пусть R — множество эквивалентности на ι. Произведение по s f равно произведению по представителям эквивалентных классов (как и в предыдущей формуле разбиения), т. е. то же выражение, что и в предыдущем разбиении.
LaTeX
$$$\\prod_{x \\in s} f(x) = \\prod_{xbar \\in s.image(\\mathrm{Quotient.mk} R)} \\left( \\prod_{y \\in s, \\; \\langle y \\rangle = xbar} f(y) \\right)$$$
Lean4
/-- A product can be partitioned into a product of products, each equivalent under a setoid. -/
@[to_additive /-- A sum can be partitioned into a sum of sums, each equivalent under a setoid. -/
]
theorem prod_partition (R : Setoid ι) [DecidableRel R.r] :
∏ x ∈ s, f x = ∏ xbar ∈ s.image (Quotient.mk _), ∏ y ∈ s with ⟦y⟧ = xbar, f y :=
by
refine (Finset.prod_image' f fun x _hx => ?_).symm
rfl
