doc-next-gen

Mathlib.Algebra.Regular.Basic

Module docstring

{"# Regular elements

We introduce left-regular, right-regular and regular elements, along with their to_additive analogues add-left-regular, add-right-regular and add-regular elements.

By definition, a regular element in a commutative ring is a non-zero divisor. Lemma isRegular_of_ne_zero implies that every non-zero element of an integral domain is regular. Since it assumes that the ring is a CancelMonoidWithZero it applies also, for instance, to ℕ.

The lemmas in Section MulZeroClass show that the 0 element is (left/right-)regular if and only if the MulZeroClass is trivial. This is useful when figuring out stopping conditions for regular sequences: if 0 is ever an element of a regular sequence, then we can extend the sequence by adding one further 0.

The final goal is to develop part of the API to prove, eventually, results about non-zero-divisors. "}

IsLeftRegular definition
(c : R)
Full source 
/-- A left-regular element is an element `c` such that multiplication on the left by `c`
is injective. -/
@[to_additive "An add-left-regular element is an element `c` such that addition
    on the left by `c` is injective."]
def IsLeftRegular (c : R) :=
  (c * ·).Injective
Left-regular element
Informal description
An element \( c \) in a multiplicative structure \( R \) is called *left-regular* if left multiplication by \( c \) is injective. That is, for any \( x, y \in R \), \( c \cdot x = c \cdot y \) implies \( x = y \).
IsRightRegular definition
(c : R)
Full source 
/-- A right-regular element is an element `c` such that multiplication on the right by `c`
is injective. -/
@[to_additive "An add-right-regular element is an element `c` such that addition
    on the right by `c` is injective."]
def IsRightRegular (c : R) :=
  (· * c).Injective
Right-regular element in a multiplicative structure
Informal description
An element \( c \) in a multiplicative structure \( R \) is called *right-regular* if right multiplication by \( c \) is injective. That is, for any \( x, y \in R \), \( x \cdot c = y \cdot c \) implies \( x = y \).
IsAddRegular structure
{R : Type*} [Add R] (c : R)
Full source 
/-- An add-regular element is an element `c` such that addition by `c` both on the left and
on the right is injective. -/
structure IsAddRegular {R : Type*} [Add R] (c : R) : Prop where
  /-- An add-regular element `c` is left-regular -/
  left : IsAddLeftRegular c -- Porting note: It seems like to_additive is misbehaving
  /-- An add-regular element `c` is right-regular -/
  right : IsAddRightRegular c
Add-regular element
Informal description
An element \( c \) in an additive structure \( R \) is called *add-regular* if both left and right addition by \( c \) are injective. That is, for any \( x, y \in R \), \( c + x = c + y \) implies \( x = y \) and \( x + c = y + c \) implies \( x = y \).
IsRegular structure
(c : R)
Full source 
/-- A regular element is an element `c` such that multiplication by `c` both on the left and
on the right is injective. -/
structure IsRegular (c : R) : Prop where
  /-- A regular element `c` is left-regular -/
  left : IsLeftRegular c
  /-- A regular element `c` is right-regular -/
  right : IsRightRegular c
Regular element in a multiplicative structure
Informal description
An element \( c \) of a multiplicative structure \( R \) is called *regular* if both left and right multiplication by \( c \) are injective functions. That is, for all \( x, y \in R \), \( c \cdot x = c \cdot y \) implies \( x = y \) (left regularity), and \( x \cdot c = y \cdot c \) implies \( x = y \) (right regularity).
isRegular_iff theorem
{c : R} : IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c
Full source 
@[to_additive]
theorem isRegular_iff {c : R} : IsRegularIsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c :=
  ⟨fun ⟨h1, h2⟩ => ⟨h1, h2⟩, fun ⟨h1, h2⟩ => ⟨h1, h2⟩⟩
Characterization of Regular Elements via Left and Right Regularity
Informal description
An element $c$ in a multiplicative structure $R$ is regular if and only if it is both left-regular and right-regular. That is, $c$ is regular precisely when both left multiplication by $c$ and right multiplication by $c$ are injective operations.
MulLECancellable.isLeftRegular theorem
[PartialOrder R] {a : R} (ha : MulLECancellable a) : IsLeftRegular a
Full source 
@[to_additive]
protected theorem MulLECancellable.isLeftRegular [PartialOrder R] {a : R}
    (ha : MulLECancellable a) : IsLeftRegular a :=
  ha.Injective
Left-regularity from multiplicative left order-cancellability
Informal description
Let $R$ be a type with a multiplication operation and a partial order. For any element $a \in R$ that is multiplicative left order-cancellable (i.e., $a \cdot b \leq a \cdot c$ implies $b \leq c$ for all $b, c \in R$), then $a$ is left-regular (i.e., left multiplication by $a$ is injective).
IsLeftRegular.right_of_commute theorem
{a : R} (ca : ∀ b, Commute a b) (h : IsLeftRegular a) : IsRightRegular a
Full source 
theorem IsLeftRegular.right_of_commute {a : R}
    (ca : ∀ b, Commute a b) (h : IsLeftRegular a) : IsRightRegular a :=
  fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
Right-regularity from left-regularity for commuting elements
Informal description
Let $a$ be an element in a multiplicative structure $R$ such that $a$ commutes with every element $b$ in $R$ (i.e., $a * b = b * a$ for all $b \in R$). If $a$ is left-regular (i.e., left multiplication by $a$ is injective), then $a$ is also right-regular (i.e., right multiplication by $a$ is injective).
IsRightRegular.left_of_commute theorem
{a : R} (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a
Full source 
theorem IsRightRegular.left_of_commute {a : R}
    (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a := by
  simp_rw [@Commute.symm_iff R _ a] at ca
  exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm
Left-regularity from right-regularity for commuting elements
Informal description
Let $a$ be an element in a multiplicative structure $R$ such that $a$ commutes with every element $b$ in $R$ (i.e., $a * b = b * a$ for all $b \in R$). If $a$ is right-regular (i.e., right multiplication by $a$ is injective), then $a$ is also left-regular (i.e., left multiplication by $a$ is injective).
Commute.isRightRegular_iff theorem
{a : R} (ca : ∀ b, Commute a b) : IsRightRegular a ↔ IsLeftRegular a
Full source 
theorem Commute.isRightRegular_iff {a : R} (ca : ∀ b, Commute a b) :
    IsRightRegularIsRightRegular a ↔ IsLeftRegular a :=
  ⟨IsRightRegular.left_of_commute ca, IsLeftRegular.right_of_commute ca⟩
Equivalence of Left and Right Regularity for Commuting Elements: $\text{IsRightRegular}(a) \leftrightarrow \text{IsLeftRegular}(a)$
Informal description
Let $a$ be an element in a multiplicative structure $R$ such that $a$ commutes with every element $b$ in $R$ (i.e., $a * b = b * a$ for all $b \in R$). Then $a$ is right-regular (right multiplication by $a$ is injective) if and only if $a$ is left-regular (left multiplication by $a$ is injective).
Commute.isRegular_iff theorem
{a : R} (ca : ∀ b, Commute a b) : IsRegular a ↔ IsLeftRegular a
Full source 
theorem Commute.isRegular_iff {a : R} (ca : ∀ b, Commute a b) : IsRegularIsRegular a ↔ IsLeftRegular a :=
  ⟨fun h => h.left, fun h => ⟨h, h.right_of_commute ca⟩⟩
Regularity Equivalence for Commuting Elements: $\text{IsRegular}(a) \leftrightarrow \text{IsLeftRegular}(a)$
Informal description
Let $a$ be an element in a multiplicative structure $R$ such that $a$ commutes with every element $b$ in $R$ (i.e., $a * b = b * a$ for all $b \in R$). Then $a$ is regular (both left and right multiplication by $a$ are injective) if and only if $a$ is left-regular (left multiplication by $a$ is injective).
IsLeftRegular.mul theorem
(lra : IsLeftRegular a) (lrb : IsLeftRegular b) : IsLeftRegular (a * b)
Full source 
/-- In a semigroup, the product of left-regular elements is left-regular. -/
@[to_additive "In an additive semigroup, the sum of add-left-regular elements is add-left.regular."]
theorem IsLeftRegular.mul (lra : IsLeftRegular a) (lrb : IsLeftRegular b) : IsLeftRegular (a * b) :=
  show Function.Injective (((a * b) * ·)) from comp_mul_left a b ▸ lra.comp lrb
Product of Left-Regular Elements is Left-Regular
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If $a$ and $b$ are left-regular (i.e., left multiplication by $a$ and $b$ are injective), then their product $a * b$ is also left-regular.
IsRightRegular.mul theorem
(rra : IsRightRegular a) (rrb : IsRightRegular b) : IsRightRegular (a * b)
Full source 
/-- In a semigroup, the product of right-regular elements is right-regular. -/
@[to_additive "In an additive semigroup, the sum of add-right-regular elements is
add-right-regular."]
theorem IsRightRegular.mul (rra : IsRightRegular a) (rrb : IsRightRegular b) :
    IsRightRegular (a * b) :=
  show Function.Injective (· * (a * b)) from comp_mul_right b a ▸ rrb.comp rra
Product of Right-Regular Elements is Right-Regular
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If $a$ and $b$ are right-regular (i.e., right multiplication by $a$ and $b$ are injective), then their product $a * b$ is also right-regular.
IsRegular.mul theorem
(rra : IsRegular a) (rrb : IsRegular b) : IsRegular (a * b)
Full source 
/-- In a semigroup, the product of regular elements is regular. -/
@[to_additive "In an additive semigroup, the sum of add-regular elements is add-regular."]
theorem IsRegular.mul (rra : IsRegular a) (rrb : IsRegular b) :
    IsRegular (a * b) :=
  ⟨rra.left.mul rrb.left, rra.right.mul rrb.right⟩
Product of Regular Elements is Regular in a Semigroup
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If $a$ and $b$ are regular (i.e., both left and right multiplication by $a$ and $b$ are injective), then their product $a * b$ is also regular.
IsLeftRegular.of_mul theorem
(ab : IsLeftRegular (a * b)) : IsLeftRegular b
Full source 
/-- If an element `b` becomes left-regular after multiplying it on the left by a left-regular
element, then `b` is left-regular. -/
@[to_additive "If an element `b` becomes add-left-regular after adding to it on the left
an add-left-regular element, then `b` is add-left-regular."]
theorem IsLeftRegular.of_mul (ab : IsLeftRegular (a * b)) : IsLeftRegular b :=
  Function.Injective.of_comp (f := (a * ·)) (by rwa [comp_mul_left a b])
Left-regularity of factor from left-regularity of product
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If the product $a * b$ is left-regular (i.e., left multiplication by $a * b$ is injective), then $b$ is left-regular.
mul_isLeftRegular_iff theorem
(b : R) (ha : IsLeftRegular a) : IsLeftRegular (a * b) ↔ IsLeftRegular b
Full source 
/-- An element is left-regular if and only if multiplying it on the left by a left-regular element
is left-regular. -/
@[to_additive (attr := simp) "An element is add-left-regular if and only if adding to it on the left
an add-left-regular element is add-left-regular."]
theorem mul_isLeftRegular_iff (b : R) (ha : IsLeftRegular a) :
    IsLeftRegularIsLeftRegular (a * b) ↔ IsLeftRegular b :=
  ⟨fun ab => IsLeftRegular.of_mul ab, fun ab => IsLeftRegular.mul ha ab⟩
Left-regularity of product $a \cdot b$ is equivalent to left-regularity of $b$ when $a$ is left-regular
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If $a$ is left-regular, then the product $a \cdot b$ is left-regular if and only if $b$ is left-regular.
IsRightRegular.of_mul theorem
(ab : IsRightRegular (b * a)) : IsRightRegular b
Full source 
/-- If an element `b` becomes right-regular after multiplying it on the right by a right-regular
element, then `b` is right-regular. -/
@[to_additive "If an element `b` becomes add-right-regular after adding to it on the right
an add-right-regular element, then `b` is add-right-regular."]
theorem IsRightRegular.of_mul (ab : IsRightRegular (b * a)) : IsRightRegular b := by
  refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))
  rw [← mul_assoc, ← mul_assoc]
  exact congr_arg (· * a) xy
Right-regularity of factor from right-regularity of product
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If the product $b \cdot a$ is right-regular (i.e., right multiplication by $b \cdot a$ is injective), then $b$ is right-regular.
mul_isRightRegular_iff theorem
(b : R) (ha : IsRightRegular a) : IsRightRegular (b * a) ↔ IsRightRegular b
Full source 
/-- An element is right-regular if and only if multiplying it on the right with a right-regular
element is right-regular. -/
@[to_additive (attr := simp)
"An element is add-right-regular if and only if adding it on the right to
an add-right-regular element is add-right-regular."]
theorem mul_isRightRegular_iff (b : R) (ha : IsRightRegular a) :
    IsRightRegularIsRightRegular (b * a) ↔ IsRightRegular b :=
  ⟨fun ab => IsRightRegular.of_mul ab, fun ab => IsRightRegular.mul ab ha⟩
Right-regularity of product $b \cdot a$ is equivalent to right-regularity of $b$ when $a$ is right-regular
Informal description
Let $a$ and $b$ be elements of a semigroup $R$. If $a$ is right-regular, then the product $b \cdot a$ is right-regular if and only if $b$ is right-regular.
isRegular_mul_and_mul_iff theorem
: IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
Full source 
/-- Two elements `a` and `b` are regular if and only if both products `a * b` and `b * a`
are regular. -/
@[to_additive "Two elements `a` and `b` are add-regular if and only if both sums `a + b` and
`b + a` are add-regular."]
theorem isRegular_mul_and_mul_iff :
    IsRegularIsRegular (a * b) ∧ IsRegular (b * a)IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b := by
  refine ⟨?_, ?_⟩
  · rintro ⟨ab, ba⟩
    exact
      ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
  · rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩
Regularity of Products and Factors in a Semigroup: $IsRegular(a * b) ∧ IsRegular(b * a) ↔ IsRegular(a) ∧ IsRegular(b)$
Informal description
For elements $a$ and $b$ in a semigroup $R$, the products $a * b$ and $b * a$ are both regular if and only if both $a$ and $b$ are regular.
IsRegular.and_of_mul_of_mul theorem
(ab : IsRegular (a * b)) (ba : IsRegular (b * a)) : IsRegular a ∧ IsRegular b
Full source 
/-- The "most used" implication of `mul_and_mul_iff`, with split hypotheses, instead of `∧`. -/
@[to_additive "The \"most used\" implication of `add_and_add_iff`, with split
hypotheses, instead of `∧`."]
theorem IsRegular.and_of_mul_of_mul (ab : IsRegular (a * b)) (ba : IsRegular (b * a)) :
    IsRegularIsRegular a ∧ IsRegular b :=
  isRegular_mul_and_mul_iff.mp ⟨ab, ba⟩
Regularity of Factors Implied by Regularity of Products
Informal description
For elements $a$ and $b$ in a semigroup $R$, if both products $a * b$ and $b * a$ are regular, then both $a$ and $b$ are regular.
IsLeftRegular.subsingleton theorem
(h : IsLeftRegular (0 : R)) : Subsingleton R
Full source 
/-- The element `0` is left-regular if and only if `R` is trivial. -/
theorem IsLeftRegular.subsingleton (h : IsLeftRegular (0 : R)) : Subsingleton R :=
  ⟨fun a b => h <| Eq.trans (zero_mul a) (zero_mul b).symm⟩
Left-regularity of zero implies subsingleton
Informal description
If the zero element $0$ in a multiplicative structure $R$ is left-regular, then $R$ is a subsingleton (i.e., all elements of $R$ are equal).
IsRightRegular.subsingleton theorem
(h : IsRightRegular (0 : R)) : Subsingleton R
Full source 
/-- The element `0` is right-regular if and only if `R` is trivial. -/
theorem IsRightRegular.subsingleton (h : IsRightRegular (0 : R)) : Subsingleton R :=
  ⟨fun a b => h <| Eq.trans (mul_zero a) (mul_zero b).symm⟩
Right-regularity of zero implies subsingleton
Informal description
If the zero element $0$ in a multiplicative structure $R$ is right-regular, then $R$ is a subsingleton (i.e., all elements of $R$ are equal).
IsRegular.subsingleton theorem
(h : IsRegular (0 : R)) : Subsingleton R
Full source 
/-- The element `0` is regular if and only if `R` is trivial. -/
theorem IsRegular.subsingleton (h : IsRegular (0 : R)) : Subsingleton R :=
  h.left.subsingleton
Regularity of Zero Implies Triviality of Structure
Informal description
If the zero element $0$ in a multiplicative structure $R$ is regular (both left- and right-regular), then $R$ is a subsingleton (i.e., all elements of $R$ are equal).
isLeftRegular_zero_iff_subsingleton theorem
: IsLeftRegular (0 : R) ↔ Subsingleton R
Full source 
/-- The element `0` is left-regular if and only if `R` is trivial. -/
theorem isLeftRegular_zero_iff_subsingleton : IsLeftRegularIsLeftRegular (0 : R) ↔ Subsingleton R :=
  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
Left-regularity of zero is equivalent to triviality of $R$
Informal description
The zero element $0$ in a multiplicative structure $R$ is left-regular if and only if $R$ is a subsingleton (i.e., all elements of $R$ are equal).
not_isLeftRegular_zero_iff theorem
: ¬IsLeftRegular (0 : R) ↔ Nontrivial R
Full source 
/-- In a non-trivial `MulZeroClass`, the `0` element is not left-regular. -/
theorem not_isLeftRegular_zero_iff : ¬IsLeftRegular (0 : R)¬IsLeftRegular (0 : R) ↔ Nontrivial R := by
  rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
  push_neg
  exact Iff.rfl
Non-left-regularity of zero is equivalent to nontriviality of $R$
Informal description
In a multiplicative structure $R$ with zero, the zero element $0$ is not left-regular if and only if $R$ is nontrivial (i.e., contains at least two distinct elements).
isRightRegular_zero_iff_subsingleton theorem
: IsRightRegular (0 : R) ↔ Subsingleton R
Full source 
/-- The element `0` is right-regular if and only if `R` is trivial. -/
theorem isRightRegular_zero_iff_subsingleton : IsRightRegularIsRightRegular (0 : R) ↔ Subsingleton R :=
  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩
Right-regularity of zero is equivalent to subsingleton structure
Informal description
The zero element $0$ in a multiplicative structure $R$ is right-regular if and only if $R$ is a subsingleton (i.e., all elements of $R$ are equal).
not_isRightRegular_zero_iff theorem
: ¬IsRightRegular (0 : R) ↔ Nontrivial R
Full source 
/-- In a non-trivial `MulZeroClass`, the `0` element is not right-regular. -/
theorem not_isRightRegular_zero_iff : ¬IsRightRegular (0 : R)¬IsRightRegular (0 : R) ↔ Nontrivial R := by
  rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
  push_neg
  exact Iff.rfl
Non-right-regularity of zero in nontrivial structures: $\neg\text{IsRightRegular}(0) \leftrightarrow \text{Nontrivial}\,R$
Informal description
In a multiplicative structure $R$ with zero, the zero element $0$ is not right-regular if and only if $R$ is nontrivial (i.e., contains at least two distinct elements).
isRegular_iff_subsingleton theorem
: IsRegular (0 : R) ↔ Subsingleton R
Full source 
/-- The element `0` is regular if and only if `R` is trivial. -/
theorem isRegular_iff_subsingleton : IsRegularIsRegular (0 : R) ↔ Subsingleton R :=
  ⟨fun h => h.left.subsingleton, fun h =>
    ⟨isLeftRegular_zero_iff_subsingleton.mpr h, isRightRegular_zero_iff_subsingleton.mpr h⟩⟩
Regularity of Zero is Equivalent to Triviality of $R$
Informal description
The zero element $0$ in a multiplicative structure $R$ is regular (both left-regular and right-regular) if and only if $R$ is a subsingleton (i.e., all elements of $R$ are equal).
IsLeftRegular.ne_zero theorem
[Nontrivial R] (la : IsLeftRegular a) : a ≠ 0
Full source 
/-- A left-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
theorem IsLeftRegular.ne_zero [Nontrivial R] (la : IsLeftRegular a) : a ≠ 0 := by
  rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (la (?_ : 0 * x = 0 * y)) -- Porting note: lean4 seems to need the type signature
  rw [zero_mul, zero_mul]
Left-regular elements are nonzero in nontrivial structures
Informal description
In a nontrivial multiplicative structure $R$ with zero, if an element $a \in R$ is left-regular (i.e., left multiplication by $a$ is injective), then $a$ is nonzero, i.e., $a \neq 0$.
IsRightRegular.ne_zero theorem
[Nontrivial R] (ra : IsRightRegular a) : a ≠ 0
Full source 
/-- A right-regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
theorem IsRightRegular.ne_zero [Nontrivial R] (ra : IsRightRegular a) : a ≠ 0 := by
  rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (ra (?_ : x * 0 = y * 0))
  rw [mul_zero, mul_zero]
Right-regular elements are nonzero in nontrivial structures
Informal description
In a nontrivial multiplicative structure $R$ with zero, if an element $a \in R$ is right-regular (i.e., right multiplication by $a$ is injective), then $a$ is nonzero.
IsRegular.ne_zero theorem
[Nontrivial R] (la : IsRegular a) : a ≠ 0
Full source 
/-- A regular element of a `Nontrivial` `MulZeroClass` is non-zero. -/
theorem IsRegular.ne_zero [Nontrivial R] (la : IsRegular a) : a ≠ 0 :=
  la.left.ne_zero
Regular Elements are Nonzero in Nontrivial Structures
Informal description
In a nontrivial multiplicative structure $R$ with zero, if an element $a \in R$ is regular (i.e., both left and right multiplication by $a$ are injective), then $a$ is nonzero, i.e., $a \neq 0$.
not_isLeftRegular_zero theorem
[nR : Nontrivial R] : ¬IsLeftRegular (0 : R)
Full source 
/-- In a non-trivial ring, the element `0` is not left-regular -- with typeclasses. -/
theorem not_isLeftRegular_zero [nR : Nontrivial R] : ¬IsLeftRegular (0 : R) :=
  not_isLeftRegular_zero_iff.mpr nR
Non-left-regularity of zero in nontrivial rings
Informal description
In a nontrivial ring $R$, the zero element $0$ is not left-regular, i.e., left multiplication by $0$ is not injective.
not_isRightRegular_zero theorem
[nR : Nontrivial R] : ¬IsRightRegular (0 : R)
Full source 
/-- In a non-trivial ring, the element `0` is not right-regular -- with typeclasses. -/
theorem not_isRightRegular_zero [nR : Nontrivial R] : ¬IsRightRegular (0 : R) :=
  not_isRightRegular_zero_iff.mpr nR
Non-right-regularity of Zero in Nontrivial Rings
Informal description
In a nontrivial ring $R$, the zero element $0$ is not right-regular, i.e., right multiplication by $0$ is not injective.
not_isRegular_zero theorem
[Nontrivial R] : ¬IsRegular (0 : R)
Full source 
/-- In a non-trivial ring, the element `0` is not regular -- with typeclasses. -/
theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRegular.ne_zero h rfl
Non-regularity of Zero in Nontrivial Rings
Informal description
In a nontrivial ring $R$, the zero element $0$ is not regular, i.e., it does not satisfy the condition that both left and right multiplication by $0$ are injective functions.
IsLeftRegular.mul_left_eq_zero_iff theorem
(hb : IsLeftRegular b) : b * a = 0 ↔ a = 0
Full source 
@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
  nth_rw 1 [← mul_zero b]
  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
Left-regular elements annihilate zero if and only if they are zero
Informal description
For any element $b$ in a multiplicative structure $R$, if $b$ is left-regular (i.e., left multiplication by $b$ is injective), then for any element $a \in R$, the equation $b \cdot a = 0$ holds if and only if $a = 0$.
IsRightRegular.mul_right_eq_zero_iff theorem
(hb : IsRightRegular b) : a * b = 0 ↔ a = 0
Full source 
@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
  nth_rw 1 [← zero_mul b]
  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩
Right-regular elements annihilate zero if and only if they are zero
Informal description
For any element $b$ in a multiplicative structure $R$, if $b$ is right-regular (i.e., right multiplication by $b$ is injective), then for any element $a \in R$, the equation $a \cdot b = 0$ holds if and only if $a = 0$.
isRegular_one theorem
: IsRegular (1 : R)
Full source 
/-- If multiplying by `1` on either side is the identity, `1` is regular. -/
@[to_additive "If adding `0` on either side is the identity, `0` is regular."]
theorem isRegular_one : IsRegular (1 : R) :=
  ⟨fun a b ab => (one_mul a).symm.trans (Eq.trans ab (one_mul b)), fun a b ab =>
    (mul_one a).symm.trans (Eq.trans ab (mul_one b))⟩
Regularity of the Multiplicative Identity
Informal description
The multiplicative identity element $1$ in a multiplicative structure $R$ is regular, meaning that both left and right multiplication by $1$ are injective functions.
isRegular_mul_iff theorem
: IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
Full source 
/-- A product is regular if and only if the factors are. -/
@[to_additive "A sum is add-regular if and only if the summands are."]
theorem isRegular_mul_iff : IsRegularIsRegular (a * b) ↔ IsRegular a ∧ IsRegular b := by
  refine Iff.trans ?_ isRegular_mul_and_mul_iff
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
Regularity of Product $\leftrightarrow$ Regularity of Factors: $IsRegular(a * b) \leftrightarrow IsRegular(a) \land IsRegular(b)$
Informal description
For elements $a$ and $b$ in a semigroup, the product $a * b$ is regular if and only if both $a$ and $b$ are regular.
isLeftRegular_of_mul_eq_one theorem
(h : b * a = 1) : IsLeftRegular a
Full source 
/-- An element admitting a left inverse is left-regular. -/
@[to_additive "An element admitting a left additive opposite is add-left-regular."]
theorem isLeftRegular_of_mul_eq_one (h : b * a = 1) : IsLeftRegular a :=
  IsLeftRegular.of_mul (a := b) (by rw [h]; exact isRegular_one.left)
Left-regularity from left inverse: $b * a = 1$ implies $a$ is left-regular
Informal description
Let $a$ and $b$ be elements of a monoid $R$. If $b * a = 1$, then $a$ is left-regular, meaning that left multiplication by $a$ is injective.
isRightRegular_of_mul_eq_one theorem
(h : a * b = 1) : IsRightRegular a
Full source 
/-- An element admitting a right inverse is right-regular. -/
@[to_additive "An element admitting a right additive opposite is add-right-regular."]
theorem isRightRegular_of_mul_eq_one (h : a * b = 1) : IsRightRegular a :=
  IsRightRegular.of_mul (a := b) (by rw [h]; exact isRegular_one.right)
Right-regularity of elements with right inverses
Informal description
Let $a$ and $b$ be elements of a monoid $R$. If $a$ has a right inverse $b$ (i.e., $a \cdot b = 1$), then $a$ is right-regular.
Units.isRegular theorem
(a : Rˣ) : IsRegular (a : R)
Full source 
/-- If `R` is a monoid, an element in `Rˣ` is regular. -/
@[to_additive "If `R` is an additive monoid, an element in `add_units R` is add-regular."]
theorem Units.isRegular (a : Rˣ) : IsRegular (a : R) :=
  ⟨isLeftRegular_of_mul_eq_one a.inv_mul, isRightRegular_of_mul_eq_one a.mul_inv⟩
Units are regular elements in a monoid
Informal description
Let $R$ be a monoid and let $a$ be an element of the group of units $R^\times$. Then $a$ is a regular element of $R$, meaning that both left and right multiplication by $a$ are injective operations on $R$.
IsUnit.isRegular theorem
(ua : IsUnit a) : IsRegular a
Full source 
/-- A unit in a monoid is regular. -/
@[to_additive "An additive unit in an additive monoid is add-regular."]
theorem IsUnit.isRegular (ua : IsUnit a) : IsRegular a := by
  rcases ua with ⟨a, rfl⟩
  exact Units.isRegular a
Units are Regular Elements in a Monoid
Informal description
If an element $a$ in a monoid $M$ is a unit (i.e., has a multiplicative inverse), then $a$ is regular, meaning both left and right multiplication by $a$ are injective operations on $M$.
IsLeftRegular.pow theorem
(n : ℕ) (rla : IsLeftRegular a) : IsLeftRegular (a ^ n)
Full source 
/-- Any power of a left-regular element is left-regular. -/
lemma IsLeftRegular.pow (n : ℕ) (rla : IsLeftRegular a) : IsLeftRegular (a ^ n) := by
  simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]
Powers of Left-Regular Elements are Left-Regular
Informal description
For any left-regular element $a$ in a monoid $R$ and any natural number $n$, the power $a^n$ is also left-regular. That is, if left multiplication by $a$ is injective, then left multiplication by $a^n$ is also injective.
IsRightRegular.pow theorem
(n : ℕ) (rra : IsRightRegular a) : IsRightRegular (a ^ n)
Full source 
/-- Any power of a right-regular element is right-regular. -/
lemma IsRightRegular.pow (n : ℕ) (rra : IsRightRegular a) : IsRightRegular (a ^ n) := by
  rw [IsRightRegular, ← mul_right_iterate]
  exact rra.iterate n
Powers of Right-Regular Elements are Right-Regular
Informal description
For any right-regular element $a$ in a monoid $R$ and any natural number $n$, the power $a^n$ is also right-regular. That is, if right multiplication by $a$ is injective, then right multiplication by $a^n$ is also injective.
IsRegular.pow theorem
(n : ℕ) (ra : IsRegular a) : IsRegular (a ^ n)
Full source 
/-- Any power of a regular element is regular. -/
lemma IsRegular.pow (n : ℕ) (ra : IsRegular a) : IsRegular (a ^ n) :=
  ⟨IsLeftRegular.pow n ra.left, IsRightRegular.pow n ra.right⟩
Powers of Regular Elements are Regular
Informal description
For any regular element $a$ in a monoid $R$ and any natural number $n$, the power $a^n$ is also regular. That is, if both left and right multiplication by $a$ are injective, then both left and right multiplication by $a^n$ are also injective.
IsLeftRegular.pow_iff theorem
(n0 : 0 < n) : IsLeftRegular (a ^ n) ↔ IsLeftRegular a
Full source 
/-- An element `a` is left-regular if and only if a positive power of `a` is left-regular. -/
lemma IsLeftRegular.pow_iff (n0 : 0 < n) : IsLeftRegularIsLeftRegular (a ^ n) ↔ IsLeftRegular a where
  mp := by rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]; exact .of_mul
  mpr := .pow n
Left-regularity of powers: $a^n$ is left-regular iff $a$ is left-regular for $n > 0$
Informal description
For any element $a$ in a monoid $R$ and any positive natural number $n$, the power $a^n$ is left-regular if and only if $a$ itself is left-regular. That is, left multiplication by $a^n$ is injective if and only if left multiplication by $a$ is injective.
IsRightRegular.pow_iff theorem
(n0 : 0 < n) : IsRightRegular (a ^ n) ↔ IsRightRegular a
Full source 
/-- An element `a` is right-regular if and only if a positive power of `a` is right-regular. -/
lemma IsRightRegular.pow_iff (n0 : 0 < n) : IsRightRegularIsRightRegular (a ^ n) ↔ IsRightRegular a where
  mp := by rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']; exact .of_mul
  mpr := .pow n
Right-regularity of powers: $a^n$ is right-regular iff $a$ is right-regular for $n > 0$
Informal description
For any element $a$ in a monoid $R$ and any positive natural number $n$, the power $a^n$ is right-regular if and only if $a$ itself is right-regular. That is, right multiplication by $a^n$ is injective if and only if right multiplication by $a$ is injective.
IsRegular.pow_iff theorem
{n : ℕ} (n0 : 0 < n) : IsRegular (a ^ n) ↔ IsRegular a
Full source 
/-- An element `a` is regular if and only if a positive power of `a` is regular. -/
lemma IsRegular.pow_iff {n : ℕ} (n0 : 0 < n) : IsRegularIsRegular (a ^ n) ↔ IsRegular a where
  mp h := ⟨(IsLeftRegular.pow_iff n0).mp h.left, (IsRightRegular.pow_iff n0).mp h.right⟩
  mpr h := ⟨.pow n h.left, .pow n h.right⟩
Regularity of powers: $a^n$ is regular iff $a$ is regular for $n > 0$
Informal description
For any element $a$ in a monoid $R$ and any positive natural number $n$, the power $a^n$ is regular if and only if $a$ itself is regular. That is, $a^n$ is both left-regular and right-regular if and only if $a$ is both left-regular and right-regular.
IsLeftRegular.all theorem
[Mul R] [IsLeftCancelMul R] (g : R) : IsLeftRegular g
Full source 
/-- If all multiplications cancel on the left then every element is left-regular. -/
@[to_additive "If all additions cancel on the left then every element is add-left-regular."]
theorem IsLeftRegular.all [Mul R] [IsLeftCancelMul R] (g : R) : IsLeftRegular g :=
  mul_right_injective g
All Elements are Left-Regular in Left-Cancellative Structures
Informal description
Let $R$ be a multiplicative structure with left-cancellative multiplication. Then every element $g \in R$ is left-regular, meaning that for any $x, y \in R$, if $g \cdot x = g \cdot y$ then $x = y$.
IsRightRegular.all theorem
[Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular g
Full source 
/-- If all multiplications cancel on the right then every element is right-regular. -/
@[to_additive "If all additions cancel on the right then every element is add-right-regular."]
theorem IsRightRegular.all [Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular g :=
  mul_left_injective g
All Elements are Right-Regular in Right-Cancellative Structures
Informal description
Let $R$ be a multiplicative structure with right-cancellative multiplication. Then every element $g \in R$ is right-regular, meaning that for any $x, y \in R$, if $x \cdot g = y \cdot g$ then $x = y$.
IsRegular.all theorem
[Mul R] [IsCancelMul R] (g : R) : IsRegular g
Full source 
/-- If all multiplications cancel then every element is regular. -/
@[to_additive "If all additions cancel then every element is add-regular."]
theorem IsRegular.all [Mul R] [IsCancelMul R] (g : R) : IsRegular g :=
  ⟨mul_right_injective g, mul_left_injective g⟩
All Elements are Regular in Cancellative Multiplicative Structures
Informal description
Let $R$ be a multiplicative structure with cancellative multiplication (i.e., both left and right cancellation properties hold). Then every element $g \in R$ is regular, meaning that for any $x, y \in R$, both $g \cdot x = g \cdot y$ implies $x = y$ and $x \cdot g = y \cdot g$ implies $x = y$.
isRegular_of_ne_zero theorem
(a0 : a ≠ 0) : IsRegular a
Full source 
/-- Non-zero elements of an integral domain are regular. -/
theorem isRegular_of_ne_zero (a0 : a ≠ 0) : IsRegular a :=
  ⟨fun _ _ => mul_left_cancel₀ a0, fun _ _ => mul_right_cancel₀ a0⟩
Nonzero Elements are Regular in Cancellative Multiplicative Structures
Informal description
For any nonzero element $a$ in a cancellative multiplicative structure with zero, $a$ is regular, meaning that both left and right multiplication by $a$ are injective.