Non-zero divisors in a ring

theorem IsLeftRegular.pow_injective {R : Type u_1} [Monoid R] {r : R} [IsMulTorsionFree R] (hx : IsLeftRegular r) (hx' : r ≠ 1) : Function.Injective fun (n : ℕ) => r ^ n

theorem IsAddLeftRegular.nsmul_injective {R : Type u_1} [AddMonoid R] {r : R} [IsAddTorsionFree R] (hx : IsAddLeftRegular r) (hx' : r ≠ 0) : Function.Injective fun (n : ℕ) => n • r

theorem IsRightRegular.pow_injective {M : Type u_2} [Monoid M] [IsMulTorsionFree M] {x : M} (hx : IsRightRegular x) (hx' : x ≠ 1) : Function.Injective fun (n : ℕ) => x ^ n

theorem IsAddRightRegular.nsmul_injective {M : Type u_2} [AddMonoid M] [IsAddTorsionFree M] {x : M} (hx : IsAddRightRegular x) (hx' : x ≠ 0) : Function.Injective fun (n : ℕ) => n • x

theorem IsMulTorsionFree.pow_right_injective {M : Type u_2} [CancelMonoid M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) : Function.Injective fun (n : ℕ) => x ^ n

@[simp]

theorem IsMulTorsionFree.pow_right_inj {M : Type u_2} [CancelMonoid M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) {n m : ℕ} : x ^ n = x ^ m ↔ n = m

theorem IsMulTorsionFree.pow_right_injective₀ {M : Type u_2} [CancelMonoidWithZero M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) (hx' : x ≠ 0) : Function.Injective fun (n : ℕ) => x ^ n

@[simp]

theorem IsMulTorsionFree.pow_right_inj₀ {M : Type u_2} [CancelMonoidWithZero M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) (hx' : x ≠ 0) {n m : ℕ} : x ^ n = x ^ m ↔ n = m

theorem IsLeftRegular.isUnit_of_finite {R : Type u_1} [Monoid R] {r : R} [Finite R] (h : IsLeftRegular r) : IsUnit r

theorem IsRightRegular.isUnit_of_finite {R : Type u_1} [Monoid R] {r : R} [Finite R] (h : IsRightRegular r) : IsUnit r

theorem isRegular_iff_isUnit_of_finite {R : Type u_1} [Monoid R] {r : R} [Finite R] : IsRegular r ↔ IsUnit r

theorem isLeftRegular_iff_mem_nonZeroDivisorsLeft {R : Type u_1} [Ring R] {r : R} : IsLeftRegular r ↔ r ∈ nonZeroDivisorsLeft R

theorem isRightRegular_iff_mem_nonZeroDivisorsRight {R : Type u_1} [Ring R] {r : R} : IsRightRegular r ↔ r ∈ nonZeroDivisorsRight R

theorem isRegular_iff_mem_nonZeroDivisors {R : Type u_1} [Ring R] {r : R} : IsRegular r ↔ r ∈ nonZeroDivisors R

theorem le_nonZeroDivisorsLeft_iff_isLeftRegular {R : Type u_1} [Ring R] {S : Submonoid R} : S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular ↑s

theorem le_nonZeroDivisorsRight_iff_isRightRegular {R : Type u_1} [Ring R] {S : Submonoid R} : S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular ↑s

theorem le_nonZeroDivisors_iff_isRegular {R : Type u_1} [Ring R] {S : Submonoid R} : S ≤ nonZeroDivisors R ↔ ∀ (s : ↥S), IsRegular ↑s

@[deprecated isLeftRegular_iff_mem_nonZeroDivisorsLeft (since := "2025-07-16")]

theorem isLeftRegular_iff_mem_nonZeroDivisorsRight {R : Type u_1} [Ring R] {r : R} : IsLeftRegular r ↔ r ∈ nonZeroDivisorsLeft R

Alias of isLeftRegular_iff_mem_nonZeroDivisorsLeft.

@[deprecated isRightRegular_iff_mem_nonZeroDivisorsRight (since := "2025-07-16")]

theorem isRightRegular_iff_mem_nonZeroDivisorsLeft {R : Type u_1} [Ring R] {r : R} : IsRightRegular r ↔ r ∈ nonZeroDivisorsRight R

Alias of isRightRegular_iff_mem_nonZeroDivisorsRight.

@[deprecated le_nonZeroDivisorsRight_iff_isRightRegular (since := "2025-07-16")]

theorem le_nonZeroDivisors_iff_isRightRegular {R : Type u_1} [Ring R] {S : Submonoid R} : S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular ↑s

Alias of le_nonZeroDivisorsRight_iff_isRightRegular.

theorem mul_cancel_left_mem_nonZeroDivisorsLeft {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisorsLeft R) : r * x = r * y ↔ x = y

theorem mul_cancel_right_mem_nonZeroDivisorsRight {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisorsRight R) : x * r = y * r ↔ x = y

@[simp]

theorem mul_cancel_left_mem_nonZeroDivisors {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisors R) : r * x = r * y ↔ x = y

theorem mul_cancel_left_coe_nonZeroDivisors {R : Type u_1} [Ring R] {x y : R} {c : ↥(nonZeroDivisors R)} : ↑c * x = ↑c * y ↔ x = y

theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisors R) : x * r = y * r ↔ x = y

theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_1} [Ring R] {x y : R} {c : ↥(nonZeroDivisors R)} : x * ↑c = y * ↑c ↔ x = y

theorem isUnit_iff_mem_nonZeroDivisors_of_finite {R : Type u_1} [Ring R] {a : R} [Finite R] : IsUnit a ↔ a ∈ nonZeroDivisors R

In a finite ring, an element is a unit iff it is a non-zero-divisor.

theorem dvd_cancel_left_mem_nonZeroDivisors {R : Type u_1} [Ring R] {x y r : R} (hr : r ∈ nonZeroDivisors R) : r * x ∣ r * y ↔ x ∣ y

theorem dvd_cancel_left_coe_nonZeroDivisors {R : Type u_1} [Ring R] {x y : R} {c : ↥(nonZeroDivisors R)} : ↑c * x ∣ ↑c * y ↔ x ∣ y

theorem dvd_cancel_right_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {r x y : R} (hr : r ∈ nonZeroDivisors R) : x * r ∣ y * r ↔ x ∣ y

theorem dvd_cancel_right_coe_nonZeroDivisors {R : Type u_1} [CommRing R] {x y : R} {c : ↥(nonZeroDivisors R)} : x * ↑c ∣ y * ↑c ↔ x ∣ y