English
If the element 0 lies in a list l of a monoid with zero, then the product l.prod equals 0.
Русский
Если ноль принадлежит списку l, взятому в моноиде с нулём, то произведение списка равно нулю.
LaTeX
$$$0 \in l \Rightarrow l.prod = 0$$$
Lean4
/-- If zero is an element of a list `l`, then `List.prod l = 0`. If the domain is a nontrivial
monoid with zero with no zero divisors, then this implication becomes an `iff`, see
`List.prod_eq_zero_iff`. -/
theorem prod_eq_zero :
∀ {l : List M₀},
(0 : M₀) ∈ l →
l.prod =
0
-- | absurd h (not_mem_nil _)
| a :: l, h => by
rw [prod_cons]
rcases mem_cons.1 h with ha | hl
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]
