English
If (s ∩ mulSupport (f ∘ g)).InjOn g, then ∏_{i∈g''s} f(i) = ∏_{j∈s} f(g(j)).
Русский
Если g инъективна на s ∩ mulSupport(f ∘ g), то произведение по образу равно произведению по композиции.
LaTeX
$$\operatorname{InjOn}\; g\;(s \cap \operatorname{mulSupport}(f \circ g)) \Rightarrow \prod_{i \in g'' s} f(i) = \prod_{j \in s} 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 on `mulSupport (f ∘ g)`. -/
@[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 on `support (f ∘ g)`. -/
]
theorem finprod_mem_range' {g : β → α} (hg : (mulSupport (f ∘ g)).InjOn g) : ∏ᶠ i ∈ range g, f i = ∏ᶠ j, f (g j) :=
by
rw [← image_univ, finprod_mem_image', finprod_mem_univ]
rwa [univ_inter]
