prod_eq_zero_iff — Mathlib

English

Under suitable assumptions (NoZeroDivisors, Nontrivial), s.prod = 0 if and only if 0 ∈ s.

Русский

При подходящих предположениях (NoZeroDivisors, Nontrivial) s.prod = 0 тогда и только тогда, когда 0 ∈ s.

LaTeX

$$$(NoZeroDivisors) \Rightarrow s.prod = 0 \iff 0 \in s$$$

Lean4

@[simp]
theorem prod_eq_zero_iff : s.prod = 0 ↔ (0 : M₀) ∈ s :=
  Quotient.inductionOn s fun l ↦ by rw [quot_mk_to_coe, prod_coe]; exact List.prod_eq_zero_iff

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