noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight

English

NoZeroDivisors M holds iff every nonzero element lies in the right non-zero divisors.

Русский

NoZeroDivisors M верно тогда и только тогда, когда каждый ненулевой элемент принадлежит справа не нулевым делителям.

LaTeX

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

Lean4

theorem noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight :
    NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → x ∈ nonZeroDivisorsRight M₀ :=
  noZeroDivisors_iff_left_eq_zero_of_mul

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