prod_image — Mathlib

English

If a map g is injective on a finite set s, the product of f over the image of s under g equals the product of f ∘ g over s.

Русский

Если отображение g инъективно на множестве s, то произведение по образу s равно произведению по композиции f ∘ g на s.

LaTeX

$$$\\text{If } g \\text{ is injective on } s: \\quad \\prod_{x \\in s^{\\mathrm{image}}} f(x) = \\prod_{x \\in s} f(g(x)).$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_image [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
    Set.InjOn g s → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
  fold_image

Похожие утверждения