English
If a product equals 1 and the function is 1 except possibly at one point, then the function is 1 on the entire finite set.
Русский
Если произведение равно 1, и функция равна 1 кроме одной точки, то функция равна 1 на всем множестве.
LaTeX
$$$hp : \\prod_{x \\in s} f(x) = 1 \\;\\rightarrow\\; (\\forall x \\in s, x \\neq a \\rightarrow f(x) = 1) \\rightarrow (\\forall x \\in s, f(x) = 1)$$$
Lean4
/-- If a product is 1 and the function is 1 except possibly at one
point, it is 1 everywhere on the `Finset`. -/
@[to_additive /-- If a sum is 0 and the function is 0 except possibly at one
point, it is 0 everywhere on the `Finset`. -/
]
theorem eq_one_of_prod_eq_one {s : Finset ι} {f : ι → M} {a : ι} (hp : ∏ x ∈ s, f x = 1)
(h1 : ∀ x ∈ s, x ≠ a → f x = 1) : ∀ x ∈ s, f x = 1 :=
by
intro x hx
classical
by_cases h : x = a
· rw [h]
rw [h] at hx
rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha), prod_singleton] at hp
exact hp
· exact h1 x hx h
