prod_ne_zero — Mathlib

English

Let M0 be a commutative monoid with zero, with no zero divisors and nontrivial. Then for every multiset s of M0 with 0 not in s, the product of its elements is nonzero.

Русский

Пусть M₀ — коммутативный моноид с нулём без делителей нуля и ненулевой. Тогда для каждого мультимножества s над M₀, не содержащего нулевого элемента, произведение всех его элементов не равно нулю.

LaTeX

$$$$\forall s \in \mathrm{Multiset}(M_0),\ (0 \notin s) \Rightarrow \mathrm{prod}(s) \neq 0.$$$$

Lean4

theorem prod_ne_zero (h : (0 : M₀) ∉ s) : s.prod ≠ 0 :=
  mt prod_eq_zero_iff.1 h

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