English
Let s be a finite set, and f: ι → M. If there exists an involution g on s such that for every a in s, f(a) f(g(a)) = 1, and if f(a) ≠ 1 then g(a) ≠ a, and g maps s into s with g(g(a)) = a, then the product over s of f(x) equals 1.
Русский
Пусть s — конечное множество и f: ι→M. Пусть существует инволюция g на s such that для каждого a в s выполняется f(a) f(g(a)) = 1, и если f(a) ≠ 1, то g(a) ≠ a, и g отображает s в s так, что g(g(a)) = a. Тогда произведение по 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
/-- The difference with `Finset.prod_ninvolution` is that the involution is allowed to use
membership of the domain of the product, rather than being a non-dependent function. -/
@[to_additive /-- The difference with `Finset.sum_ninvolution` is that the involution is allowed to
use membership of the domain of the sum, rather than being a non-dependent function. -/
]
theorem prod_involution (g : ∀ a ∈ s, ι) (hg₁ : ∀ a ha, f a * f (g a ha) = 1) (hg₃ : ∀ a ha, f a ≠ 1 → g a ha ≠ a)
(g_mem : ∀ a ha, g a ha ∈ s) (hg₄ : ∀ a ha, g (g a ha) (g_mem a ha) = a) : ∏ x ∈ s, f x = 1 := by
classical
induction s using Finset.strongInduction with
| H s ih => ?_
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
· simp
have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]
suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1
by
rw [← prod_sdiff this, h, one_mul]
cases eq_or_ne (g x hx) x with
| inl hx' => simpa [hx'] using hg₃ x hx
| inr hx' => grind
suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _ (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃
(fun _ _ => hg₄ _ _)
grind
