prod_eq_zero_iff — Mathlib

English

Under suitable assumptions (nontrivial, NoZeroDivisors), the product of a list is zero if and only if 0 occurs in the list.

Русский

При подходящих предположениях (непустой, без нулевых делителей) произведение списка равно нулю тогда и только тогда, когда 0 встречается в списке.

LaTeX

$$$\text{NoZeroDivisors} \Rightarrow (l.prod = 0 \iff 0 \in l)$$$

Lean4

/-- Product of elements of a list `l` equals zero if and only if `0 ∈ l`. See also
`List.prod_eq_zero` for an implication that needs weaker typeclass assumptions. -/
@[simp]
theorem prod_eq_zero_iff : ∀ {l : List M₀}, l.prod = 0 ↔ (0 : M₀) ∈ l
  | [] => by simp
  | a :: l => by rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]

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