English
Let R be a setoid (equivalence relation) on ι. Then the product over a finite set s of f(x) can be written as the product over the quotient classes x̄ in s.image (Quotient.mk R) of the products over y ∈ s that lie in the class x̄ of f(y).
Русский
Пусть R — множество эквивалентности на ι. Тогда произведение по x∈s f(x) можно записать как произведение по классам эквивалентности x̄ на s, взятым в образе quotient, где внутри каждого класса берется произведение по y∈s с ⟦y⟧ = x̄.
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
/-- The product of the composition of functions `f` and `g`, is the product over `b ∈ s.image g` of
`f b` to the power of the cardinality of the fibre of `b`. See also `Finset.prod_image`. -/
@[to_additive /-- The sum of the composition of functions `f` and `g`, is the sum over
`b ∈ s.image g` of `f b` times of the cardinality of the fibre of `b`. See also
`Finset.sum_image`. -/
]
theorem prod_comp [DecidableEq κ] (f : κ → M) (g : ι → κ) :
∏ a ∈ s, f (g a) = ∏ b ∈ s.image g, f b ^ #({a ∈ s | g a = b}) := by
simp_rw [← prod_const, prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _]
