Lemmas about regular elements in rings.

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

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

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} [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} (hk : k ≠ 0) : IsRegular k

theorem isRegular_iff_ne_zero' {α : Type u_1} [Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α} : IsRegular k ↔ k ≠ 0

@[reducible, inline]

abbrev NoZeroDivisors.toCancelMonoidWithZero {α : Type u_1} [Ring α] [NoZeroDivisors α] : CancelMonoidWithZero α

A ring with no zero divisors is a CancelMonoidWithZero.

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

Equations

• NoZeroDivisors.toCancelMonoidWithZero = { toMonoidWithZero := inferInstance, toIsCancelMulZero := ⋯ }

@[reducible, inline]

abbrev NoZeroDivisors.toCancelCommMonoidWithZero {α : Type u_1} [CommRing α] [NoZeroDivisors α] : CancelCommMonoidWithZero α

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 = { toMonoid := MonoidWithZero.toMonoid, mul_comm := ⋯, toZero := MonoidWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯, toIsLeftCancelMulZero := ⋯ }

@[instance 100]

instance IsDomain.toCancelMonoidWithZero {α : Type u_1} [Semiring α] [IsDomain α] : CancelMonoidWithZero α

Equations

• IsDomain.toCancelMonoidWithZero = { toMonoidWithZero := Semiring.toMonoidWithZero, toIsCancelMulZero := ⋯ }

@[instance 100]

instance IsDomain.toCancelCommMonoidWithZero {α : Type u_1} [CommSemiring α] [IsDomain α] : CancelCommMonoidWithZero α

Equations

• IsDomain.toCancelCommMonoidWithZero = { toCommMonoidWithZero := CommSemiring.toCommMonoidWithZero, toIsLeftCancelMulZero := ⋯ }