noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft

English

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

Русский

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

LaTeX

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

Lean4

theorem noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft :
    NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → x ∈ nonZeroDivisorsLeft M₀ :=
  noZeroDivisors_iff_right_eq_zero_of_mul

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