English
In a nonunital nonassociative ring with no zero divisors, every nonzero element is regular (both left and right cancellable).
Русский
В кольце без единицы и без ассоциаций, где нет нулевых делителей, каждый ненулевой элемент регулярен (левая и правая отмена выполняются).
LaTeX
$$(hk ≠ 0) ⇒ [∀ x,y, kx = ky ⇒ x=y] ∧ [∀ x,y, xk = yk ⇒ x=y]$$
Lean4
theorem isRegular_of_ne_zero' [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} (hk : k ≠ 0) : IsRegular k :=
⟨isLeftRegular_of_non_zero_divisor k fun _ h => (NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left hk,
isRightRegular_of_non_zero_divisor k fun _ h =>
(NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hk⟩
