Documentation

Mathlib.Algebra.Ring.Regular

Lemmas about regular elements in rings. #

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

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} [inst : NonUnitalNonAssocRing α] (k : α) (h : ∀ (x : α), x * k = 0x = 0) :

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} [inst : NonUnitalNonAssocRing α] [inst : NoZeroDivisors α] {k : α} (hk : k 0) :
theorem isRegular_iff_ne_zero' {α : Type u_1} [inst : Nontrivial α] [inst : NonUnitalNonAssocRing α] [inst : NoZeroDivisors α] {k : α} :

A ring with no zero divisors is a CancelMonoidWithZero.

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

Equations
  • NoZeroDivisors.toCancelMonoidWithZero = let src := inferInstance; CancelMonoidWithZero.mk

A commutative ring with no zero divisors is a CancelCommMonoidWithZero.

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

Equations
  • NoZeroDivisors.toCancelCommMonoidWithZero = let src := NoZeroDivisors.toCancelMonoidWithZero; let src_1 := inst; CancelCommMonoidWithZero.mk
instance IsDomain.toCancelMonoidWithZero {α : Type u_1} [inst : Semiring α] [inst : IsDomain α] :
Equations
  • IsDomain.toCancelMonoidWithZero = CancelMonoidWithZero.mk
Equations
  • IsDomain.toCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk