English
If we can partition a product into blocks that each cancel to 1, then the whole product equals 1.
Русский
Если можно разбить произведение на блоки, каждый из которых даёт 1 после умножения, то всё произведение равно 1.
LaTeX
$$$\\Bigl(\\forall x \\in s,\\; \\prod_{a \\in s\\text{ with } R a x} f(a) = 1\\Bigr) \\Rightarrow \\prod_{x \\in s} f(x) = 1$$$
Lean4
/-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/
@[to_additive /-- If we can partition a sum into subsets that cancel out, then the whole sum
cancels. -/
]
theorem prod_cancels_of_partition_cancels (R : Setoid ι) [DecidableRel R] (h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1) :
∏ x ∈ s, f x = 1 := by
rw [prod_partition R, ← Finset.prod_eq_one]
intro xbar xbar_in_s
obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s
simp only [← Quotient.eq] at h
exact h x x_in_s
