Lemmas about regular elements in rings.

theorem isLeftRegular_of_non_zero_divisor {α : Type u_1} [NonUnitalNonAssocRing α] (k : α) (h : ∀ (x : α), k * x = 0 → x = 0) : IsLeftRegular k

Left Mul by a k : α over [Ring α] is injective, if k is not a zero divisor. The typeclass that restricts all terms of α to have this property is NoZeroDivisors.

theorem isRightRegular_of_non_zero_divisor {α : Type u_1} [NonUnitalNonAssocRing α] (k : α) (h : ∀ (x : α), x * k = 0 → x = 0) : IsRightRegular k

Right Mul by a k : α over [Ring α] is injective, if k is not a zero divisor. The typeclass that restricts all terms of α to have this property is NoZeroDivisors.

theorem IsRegular.of_ne_zero' {α : Type u_1} [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} (hk : k ≠ 0) : IsRegular k

@[deprecated IsRegular.of_ne_zero' (since := "2026-01-21")]

theorem isRegular_of_ne_zero' {α : Type u_1} [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} (hk : k ≠ 0) : IsRegular k

Alias of IsRegular.of_ne_zero'.

theorem isRegular_iff_ne_zero' {α : Type u_1} [Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} : IsRegular k ↔ k ≠ 0

theorem NoZeroDivisors.toIsCancelMulZero {α : Type u_1} [NonUnitalNonAssocRing α] [NoZeroDivisors α] : IsCancelMulZero α

A ring with no zero divisors is a cancellative MonoidWithZero.

Note this is not an instance as it forms a typeclass loop.

theorem IsDedekindFiniteMonoid.iff_eq_of_mul_left_eq_one {α : Type u_1} [Ring α] : IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z

A ring is Dedekind-finite if and only if every element has at most one right inverse.

theorem IsDedekindFiniteMonoid.iff_eq_of_mul_right_eq_one {α : Type u_1} [Ring α] : IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

A ring is Dedekind-finite if and only if every element has at most one left inverse.