English
In a nontrivial monoid with zero and no zero divisors, the product over a Finset is zero iff some factor is zero.
Русский
В нетривиальном моноиде с нулём и без делителей нуля произведение по Finset равно нулю тогда и только тогда, когда некоторый множитель равен нулю.
LaTeX
$$$\\forall {ι} {M₀} [\\mathsf{CommMonoidWithZero} M₀] (f: ι \\to M₀) (s: \\mathsf{Finset} ι) [\\mathsf{Nontrivial} M₀] [\\mathsf{NoZeroDivisors} M₀],\\; \\prod x\\in s, f x = 0 \\iff \\exists a \\in s, f a = 0$$$
Lean4
theorem prod_eq_zero_iff : ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0 := by
classical
induction s using Finset.induction_on with
| empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
| insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]
