English
Let s be a finite subset, and g: ι → ι with g(a) ∈ s for all a ∈ s. If for all a, f(a) f(g(a)) = 1 and for all a, f(a) ≠ 1 implies g(a) ≠ a, and g(g(a)) = a, then the product over s of f equals 1.
Русский
Пусть s — конечная подмножество, и g: ι → ι так, что для каждого a∈s выполняется g(a)∈s. Если для всех a выполняется f(a) f(g(a)) = 1 и если f(a) ≠ 1 тогда g(a) ≠ a, а также g(g(a)) = a, то произведение по x∈s f(x) = 1.
LaTeX
$$$\\Bigl(\\forall a, f(a) f(g(a)) = 1\\Bigr) \\wedge \\Bigl(\\forall a, f(a) \\neq 1 \\Rightarrow g(a) \\neq a\\Bigr) \\wedge \\Bigl(\\forall a, g(a) \\in s\\Bigr) \\wedge \\Bigl(\\forall a, g(g(a)) = a\\Bigr) \\Rightarrow \\prod_{x \\in s} f(x) = 1$$$
Lean4
/-- The difference with `Finset.prod_involution` is that the involution is a non-dependent function,
rather than being allowed to use membership of the domain of the product. -/
@[to_additive /-- The difference with `Finset.sum_involution` is that the involution is a
non-dependent function, rather than being allowed to use membership of the domain of the sum. -/
]
theorem prod_ninvolution (g : ι → ι) (hg₁ : ∀ a, f a * f (g a) = 1) (hg₂ : ∀ a, f a ≠ 1 → g a ≠ a)
(g_mem : ∀ a, g a ∈ s) (hg₃ : ∀ a, g (g a) = a) : ∏ x ∈ s, f x = 1 :=
prod_involution (fun i _ => g i) (fun i _ => hg₁ i) (fun _ _ hi => hg₂ _ hi) (fun i _ => g_mem i) (fun i _ => hg₃ i)
