prod_eq_zero — Mathlib

English

In a nontrivial commutative monoid with zero and no zero divisors, the product over a Finset is zero iff some factor is zero.

Русский

В нетривиальном коммутативном моноиде с нулём и без делителей нуля произведение по Finset равно нулю тогда и только тогда, когда существует элемент множества, который равен нулю.

LaTeX

$$$\\forall {ι}{G₀} [\\mathsf{CommMonoidWithZero} G₀] (s: \\mathsf{Finset} ι) (f: ι \\to G₀),\\; \\left(\\prod x\\in s, f x = 0\\right) \\iff \\exists a\\in s, f a = 0$$$

Lean4

theorem prod_eq_zero (hi : i ∈ s) (h : f i = 0) : ∏ j ∈ s, f j = 0 := by
  classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

Похожие утверждения