English
If the images of a map on a finite index set I are not colliding (pairwise), the product over the image of g composed with f equals the product over I of g(f(i)).
Русский
Если изображения функции на I не сталкиваются попарно, произведение по изображению g(f(i)) равно произведению по i ∈ I g(f(i)).
LaTeX
$$$\\prod_{s \\in I.image f} g(s) = \\prod_{i \\in I} g(f(i))$$$
Lean4
/-- A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 1`.
The conclusion is the same as in `prod_image`. -/
@[to_additive (attr := simp) /-- A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 0`.
The conclusion is the same as in `sum_image`. -/
]
theorem prod_image_of_pairwise_eq_one [DecidableEq ι] {f : κ → ι} {g : ι → M} {I : Finset κ}
(hf : (I : Set κ).Pairwise fun i j ↦ f i = f j → g (f i) = 1) : ∏ s ∈ I.image f, g s = ∏ i ∈ I, g (f i) :=
by
rw [prod_image']
exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm
