noZeroDivisors_iff_forall_mem_nonZeroDivisors

English

NoZeroDivisors M is equivalent to every nonzero element lying in M⁰ (the non-zero divisors).

Русский

NoZeroDivisors M эквивалентно тому, что каждый ненулевой элемент принадлежит M⁰ (не нулевые делители).

LaTeX

$$$\text{NoZeroDivisors}(M_0) \iff \forall x: M_0, x \neq 0 \rightarrow x \in M_0^{0}$$$

Lean4

theorem noZeroDivisors_iff_forall_mem_nonZeroDivisors : NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → x ∈ M₀⁰ :=
  noZeroDivisors_iff_eq_zero_of_mul

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