Mathlib.Algebra.Ring.NonZeroDivisors

mul_cancel_right_mem_nonZeroDivisors theorem

(hr : r ∈ R⁰) : x * r = y * r ↔ x = y

Full source

lemma mul_cancel_right_mem_nonZeroDivisors (hr : r ∈ R⁰) : x * r = y * r ↔ x = y := by
  refine ⟨fun h ↦ ?_, congrArg (· * r)⟩
  rw [← sub_eq_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hr, sub_mul, h, sub_self]

Right Cancellation Property for Non-zero-divisors in a Ring

Informal description

Let $R$ be a ring and let $r$ be a non-zero-divisor in $R$ (i.e., $r \in R^0$). Then for any elements $x, y \in R$, the equality $x \cdot r = y \cdot r$ holds if and only if $x = y$.

mul_cancel_right_coe_nonZeroDivisors theorem

{c : R⁰} : x * c = y * c ↔ x = y

Full source

lemma mul_cancel_right_coe_nonZeroDivisors {c : R⁰} : x * c = y * c ↔ x = y :=
  mul_cancel_right_mem_nonZeroDivisors c.prop

Right Cancellation Property for Non-zero-divisors (Coefficient Form)

Informal description

Let $R$ be a ring and let $c$ be a non-zero-divisor in $R$ (i.e., $c \in R^0$). Then for any elements $x, y \in R$, the equality $x \cdot c = y \cdot c$ holds if and only if $x = y$.

isLeftRegular_iff_mem_nonZeroDivisorsRight theorem

: IsLeftRegular r ↔ r ∈ nonZeroDivisorsRight R

Full source

lemma isLeftRegular_iff_mem_nonZeroDivisorsRight : IsLeftRegularIsLeftRegular r ↔ r ∈ nonZeroDivisorsRight R :=
  ⟨fun h r' eq ↦ h (by simp_rw [eq, mul_zero]),
    fun h r₁ r₂ eq ↦ sub_eq_zero.mp <| h _ <| by simp_rw [mul_sub, eq, sub_self]⟩

Left Cancellative Elements are Non-Right-Zero-Divisors

Informal description

An element $r$ in a ring $R$ is left regular (i.e., left cancellative) if and only if $r$ belongs to the submonoid of non-right-zero-divisors of $R$. In other words, $r$ is left cancellative if and only if for all $x \in R$, $r \cdot x = 0$ implies $x = 0$.

isRightRegular_iff_mem_nonZeroDivisorsLeft theorem

: IsRightRegular r ↔ r ∈ nonZeroDivisorsLeft R

Full source

lemma isRightRegular_iff_mem_nonZeroDivisorsLeft : IsRightRegularIsRightRegular r ↔ r ∈ nonZeroDivisorsLeft R :=
  ⟨fun h r' eq ↦ h (by simp_rw [eq, zero_mul]),
    fun h r₁ r₂ eq ↦ sub_eq_zero.mp <| h _ <| by simp_rw [sub_mul, eq, sub_self]⟩

Right Regularity Equivalence: $r$ is right regular iff $r$ is a non-left-zero-divisor

Informal description

An element $r$ in a ring $R$ is right regular (i.e., for all $x \in R$, $x \cdot r = 0$ implies $x = 0$) if and only if $r$ belongs to the submonoid of non-left-zero-divisors of $R$.

le_nonZeroDivisors_iff_isRightRegular theorem

{S : Submonoid R} : S ≤ R⁰ ↔ ∀ s : S, IsRightRegular (s : R)

Full source

lemma le_nonZeroDivisors_iff_isRightRegular {S : Submonoid R} :
    S ≤ R⁰ ↔ ∀ s : S, IsRightRegular (s : R) := by
  simp_rw [SetLike.le_def, isRightRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall,
    nonZeroDivisorsLeft_eq_nonZeroDivisors]

Submonoid Containment in Non-Zero-Divisors Equivalence: $S \leq R^0$ iff All Elements of $S$ are Right Regular

Informal description

For a submonoid $S$ of a ring $R$, $S$ is contained in the submonoid of non-zero-divisors $R^0$ if and only if every element $s \in S$ is right regular (i.e., for all $x \in R$, $x \cdot s = 0$ implies $x = 0$).

le_nonZeroDivisors_iff_isRegular theorem

{R} [CommRing R] {S : Submonoid R} : S ≤ R⁰ ↔ ∀ s : S, IsRegular (s : R)

Full source

lemma le_nonZeroDivisors_iff_isRegular {R} [CommRing R] {S : Submonoid R} :
    S ≤ R⁰ ↔ ∀ s : S, IsRegular (s : R) := by
  simp_rw [le_nonZeroDivisors_iff_isRightRegular,
    Commute.isRightRegular_iff (Commute.all _), Commute.isRegular_iff (Commute.all _)]

Submonoid of Non-Zero-Divisors Characterization via Regular Elements

Informal description

For a commutative ring $R$ and a submonoid $S$ of $R$, $S$ is contained in the submonoid of non-zero-divisors of $R$ if and only if every element $s \in S$ is a regular element (i.e., both left and right regular) in $R$.

isUnit_iff_mem_nonZeroDivisors_of_finite theorem

[Finite R] : IsUnit a ↔ a ∈ nonZeroDivisors R

Full source

/-- In a finite ring, an element is a unit iff it is a non-zero-divisor. -/
lemma isUnit_iff_mem_nonZeroDivisors_of_finite [Finite R] : IsUnitIsUnit a ↔ a ∈ nonZeroDivisors R := by
  refine ⟨IsUnit.mem_nonZeroDivisors, fun ha ↦ ?_⟩
  rw [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]
  intro b c hbc
  rw [← sub_eq_zero, ← sub_mul] at hbc
  exact sub_eq_zero.mp (ha _ hbc)

Characterization of Units as Non-Zero-Divisors in Finite Rings

Informal description

Let $R$ be a finite ring. An element $a \in R$ is a unit if and only if $a$ is a non-zero-divisor, i.e., for all $x \in R$, $a \cdot x = 0$ implies $x = 0$.

mul_cancel_left_mem_nonZeroDivisors theorem

(hr : r ∈ R⁰) : r * x = r * y ↔ x = y

Full source

@[simp]
lemma mul_cancel_left_mem_nonZeroDivisors (hr : r ∈ R⁰) : r * x = r * y ↔ x = y := by
  simp_rw [mul_comm r, mul_cancel_right_mem_nonZeroDivisors hr]

Left Cancellation Property for Non-zero-divisors in a Ring

Informal description

Let $R$ be a ring and let $r$ be a non-zero-divisor in $R$ (i.e., $r \in R^0$). Then for any elements $x, y \in R$, the equality $r \cdot x = r \cdot y$ holds if and only if $x = y$.

mul_cancel_left_coe_nonZeroDivisors theorem

{c : R⁰} : (c : R) * x = c * y ↔ x = y

Full source

lemma mul_cancel_left_coe_nonZeroDivisors {c : R⁰} : (c : R) * x = c * y ↔ x = y :=
  mul_cancel_left_mem_nonZeroDivisors c.prop

Left Cancellation Property for Non-zero-divisors in a Commutative Ring: $c \cdot x = c \cdot y \leftrightarrow x = y$

Informal description

Let $R$ be a commutative ring and let $c$ be a non-zero-divisor in $R$ (i.e., $c \in R^0$). Then for any elements $x, y \in R$, the equality $c \cdot x = c \cdot y$ holds if and only if $x = y$.

dvd_cancel_right_mem_nonZeroDivisors theorem

(hr : r ∈ R⁰) : x * r ∣ y * r ↔ x ∣ y

Full source

lemma dvd_cancel_right_mem_nonZeroDivisors (hr : r ∈ R⁰) : x * r ∣ y * rx * r ∣ y * r ↔ x ∣ y :=
  ⟨fun ⟨z, _⟩ ↦ ⟨z, by rwa [← mul_cancel_right_mem_nonZeroDivisors hr, mul_assoc, mul_comm z r,
    ← mul_assoc]⟩, fun ⟨z, h⟩ ↦ ⟨z, by rw [h, mul_assoc, mul_comm z r, ← mul_assoc]⟩⟩

Divisibility Cancellation Property for Non-zero-divisors: $x \cdot r \mid y \cdot r \leftrightarrow x \mid y$

Informal description

Let $R$ be a commutative ring and let $r$ be a non-zero-divisor in $R$ (i.e., $r \in R^0$). Then for any elements $x, y \in R$, the divisibility relation $x \cdot r \mid y \cdot r$ holds if and only if $x \mid y$.

dvd_cancel_right_coe_nonZeroDivisors theorem

{c : R⁰} : x * c ∣ y * c ↔ x ∣ y

Full source

lemma dvd_cancel_right_coe_nonZeroDivisors {c : R⁰} : x * c ∣ y * cx * c ∣ y * c ↔ x ∣ y :=
  dvd_cancel_right_mem_nonZeroDivisors c.prop

Divisibility Cancellation Property for Non-zero-divisors: $x \cdot c \mid y \cdot c \leftrightarrow x \mid y$

Informal description

Let $R$ be a commutative ring and let $c$ be a non-zero-divisor in $R$ (i.e., $c \in R^0$). Then for any elements $x, y \in R$, the divisibility relation $x \cdot c \mid y \cdot c$ holds if and only if $x \mid y$.

dvd_cancel_left_mem_nonZeroDivisors theorem

(hr : r ∈ R⁰) : r * x ∣ r * y ↔ x ∣ y

Full source

lemma dvd_cancel_left_mem_nonZeroDivisors (hr : r ∈ R⁰) : r * x ∣ r * yr * x ∣ r * y ↔ x ∣ y :=
  ⟨fun ⟨z, _⟩ ↦ ⟨z, by rwa [← mul_cancel_left_mem_nonZeroDivisors hr, ← mul_assoc]⟩,
    fun ⟨z, h⟩ ↦ ⟨z, by rw [h, ← mul_assoc]⟩⟩

Divisibility Cancellation Property for Non-zero-divisors: $r \cdot x \mid r \cdot y \leftrightarrow x \mid y$

Informal description

Let $R$ be a commutative ring and let $r$ be a non-zero-divisor in $R$ (i.e., $r$ does not divide zero). Then for any elements $x, y \in R$, the divisibility relation $r \cdot x \mid r \cdot y$ holds if and only if $x \mid y$.

dvd_cancel_left_coe_nonZeroDivisors theorem

{c : R⁰} : c * x ∣ c * y ↔ x ∣ y

Full source

lemma dvd_cancel_left_coe_nonZeroDivisors {c : R⁰} : c * x ∣ c * yc * x ∣ c * y ↔ x ∣ y :=
  dvd_cancel_left_mem_nonZeroDivisors c.prop

Divisibility Cancellation Property for Non-zero-divisors: $c \cdot x \mid c \cdot y \leftrightarrow x \mid y$

Informal description

Let $R$ be a commutative ring and let $c$ be a non-zero-divisor in $R$ (i.e., $c \in R^0$). Then for any elements $x, y \in R$, the divisibility relation $c \cdot x \mid c \cdot y$ holds if and only if $x \mid y$.