English
If (mulSupport (f ∘ g)).InjOn g, then ∏_{i∈range g} f(i) = ∏_{j} f(g(j)).
Русский
Если mulSupport(f ∘ g) инъективна на g, то произведение по диапазону равно произведению по композиции.
LaTeX
$$\operatorname{InjOn}\; g\; (\operatorname{mulSupport}(f \circ g)) \Rightarrow \prod_{i \in \operatorname{range} g} f(i) = \prod_{j} f(g(j))$$
Lean4
/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
provided that `g` is injective. -/
@[to_additive /-- The sum of `f y` over `y ∈ Set.range g` equals the sum of `f (g i)` over all `i`
provided that `g` is injective. -/
]
theorem finprod_mem_range {g : β → α} (hg : Injective g) : ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j) :=
finprod_mem_range' hg.injOn
