doc-next-gen

Mathlib.Algebra.Ring.Regular

Module docstring

{"# Lemmas about regular elements in rings. "}

isLeftRegular_of_non_zero_divisor theorem
[NonUnitalNonAssocRing α] (k : α) (h : ∀ x : α, k * x = 0 → x = 0) : IsLeftRegular k
Full source 
/-- 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 isLeftRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α)
    (h : ∀ x : α, k * x = 0 → x = 0) : IsLeftRegular k := by
  refine fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)
  rw [mul_sub, sub_eq_zero, h']
Injectivity of Left Multiplication by Non-Zero-Divisor in Non-Unital Non-Associative Rings
Informal description
Let $\alpha$ be a non-unital non-associative ring. For any element $k \in \alpha$, if $k$ is not a left zero divisor (i.e., for all $x \in \alpha$, $k \cdot x = 0$ implies $x = 0$), then left multiplication by $k$ is injective.
isRightRegular_of_non_zero_divisor theorem
[NonUnitalNonAssocRing α] (k : α) (h : ∀ x : α, x * k = 0 → x = 0) : IsRightRegular k
Full source 
/-- 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 isRightRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α)
    (h : ∀ x : α, x * k = 0 → x = 0) : IsRightRegular k := by
  refine fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)
  rw [sub_mul, sub_eq_zero, h']
Right regularity from non-zero divisor property in non-unital non-associative rings
Informal description
Let $\alpha$ be a non-unital non-associative ring. For any element $k \in \alpha$, if for all $x \in \alpha$, $x \cdot k = 0$ implies $x = 0$, then right multiplication by $k$ is injective (i.e., $k$ is right regular).
isRegular_of_ne_zero' theorem
[NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} (hk : k ≠ 0) : IsRegular k
Full source 
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⟩
Nonzero Elements are Regular in Rings without Zero Divisors
Informal description
Let $\alpha$ be a non-unital non-associative ring with no zero divisors. For any nonzero element $k \in \alpha$, $k$ is both left and right regular (i.e., multiplication by $k$ is injective on both sides).
isRegular_iff_ne_zero' theorem
[Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} : IsRegular k ↔ k ≠ 0
Full source 
theorem isRegular_iff_ne_zero' [Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α]
    {k : α} : IsRegularIsRegular k ↔ k ≠ 0 :=
  ⟨fun h => by
    rintro rfl
    exact not_not.mpr h.left not_isLeftRegular_zero, isRegular_of_ne_zero'⟩
Characterization of Regular Elements in Rings without Zero Divisors: $k$ is regular $\iff$ $k \neq 0$
Informal description
Let $\alpha$ be a nontrivial non-unital non-associative ring with no zero divisors. For any element $k \in \alpha$, $k$ is regular (both left and right regular) if and only if $k \neq 0$.
NoZeroDivisors.toCancelMonoidWithZero abbrev
[Ring α] [NoZeroDivisors α] : CancelMonoidWithZero α
Full source 
/-- A ring with no zero divisors is a `CancelMonoidWithZero`.

Note this is not an instance as it forms a typeclass loop. -/
abbrev NoZeroDivisors.toCancelMonoidWithZero [Ring α] [NoZeroDivisors α] : CancelMonoidWithZero α :=
  { (by infer_instance : MonoidWithZero α) with
    mul_left_cancel_of_ne_zero := fun ha =>
      @IsRegular.left _ _ _ (isRegular_of_ne_zero' ha) _ _,
    mul_right_cancel_of_ne_zero := fun hb =>
      @IsRegular.right _ _ _ (isRegular_of_ne_zero' hb) _ _ }
Cancellative Monoid with Zero Structure on Rings without Zero Divisors
Informal description
For any ring $\alpha$ with no zero divisors, $\alpha$ forms a cancellative monoid with zero.
NoZeroDivisors.toCancelCommMonoidWithZero abbrev
[CommRing α] [NoZeroDivisors α] : CancelCommMonoidWithZero α
Full source 
/-- A commutative ring with no zero divisors is a `CancelCommMonoidWithZero`.

Note this is not an instance as it forms a typeclass loop. -/
abbrev NoZeroDivisors.toCancelCommMonoidWithZero [CommRing α] [NoZeroDivisors α] :
    CancelCommMonoidWithZero α :=
  { NoZeroDivisors.toCancelMonoidWithZero, ‹CommRing α› with }
Commutative Rings without Zero Divisors are Cancelative Monoids with Zero
Informal description
For any commutative ring $\alpha$ with no zero divisors, $\alpha$ forms a cancelative commutative monoid with zero.
IsDomain.toCancelMonoidWithZero instance
[Semiring α] [IsDomain α] : CancelMonoidWithZero α
Full source 
instance (priority := 100) IsDomain.toCancelMonoidWithZero [Semiring α] [IsDomain α] :
    CancelMonoidWithZero α :=
  { }
Domains are Cancellative Monoids with Zero
Informal description
Every domain $\alpha$ (a nontrivial semiring where multiplication by any nonzero element is cancellative) is also a cancellative monoid with zero.