English
Let s be a finite set and g: ι → ι such that for all a ∈ s, f(a) f(g(a)) = 1, g(g(a)) = a, and g maps s into s with no fixed points when f(a) ≠ 1. Then ∏_{x ∈ s} f(x) = 1.
Русский
Пусть s — конечное множество и g: ι→ι удовлетворяет f(a) f(g(a)) = 1, g(g(a)) = a, и g отображает s в s без фиксированных точек там, где f(a) ≠ 1. Тогда произведение по x∈s f(x) равно 1.
LaTeX
$$$\\Bigl(\\forall a\\in s,\\ f(a) f(g(a)) = 1\\Bigr) \\wedge \\Bigl(\\forall a\\in s,\\ f(a) \\neq 1 \\Rightarrow g(a) \\neq a\\Bigr) \\wedge \\Bigl(\\forall a\\in s,\\ g(a) \\in s\\Bigr) \\wedge \\Bigl(\\forall a\\in s,\\ g(g(a)) = a\\Bigr) \\Rightarrow \\prod_{x \\in s} f(x) = 1$$$
Lean4
/-- Taking a product over `s : Finset ι` is the same as multiplying the value on a single element
`f a` by the product of `s.erase a`.
See `Multiset.prod_map_erase` for the `Multiset` version. -/
@[to_additive /-- Taking a sum over `s : Finset ι` is the same as adding the value on a single
element `f a` to the sum over `s.erase a`.
See `Multiset.sum_map_erase` for the `Multiset` version. -/
]
theorem mul_prod_erase [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
(f a * ∏ x ∈ s.erase a, f x) = ∏ x ∈ s, f x := by rw [← prod_insert (notMem_erase a s), insert_erase h]
