isRegular_iff_ne_zero' — Mathlib

English

A ring with no zero divisors yields a cancellative monoid with zero.

Русский

Кольцо без нулевых делителей образует отменяющий моноид с нулём.

LaTeX

$$($\forall a,b,c \in \alpha, c \neq 0 \wedge ac = bc \Rightarrow a=b$) and ($\forall a,b,c \in \alpha, c \neq 0 \wedge ca = cb \Rightarrow a=b$)$$

Lean4

theorem isRegular_iff_ne_zero' [Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} :
    IsRegular k ↔ k ≠ 0 :=
  ⟨fun h => by
    rintro rfl
    exact not_not.mpr h.left not_isLeftRegular_zero, isRegular_of_ne_zero'⟩

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