Lemmas about regular elements in rings. #
theorem
isLeftRegular_of_non_zero_divisor
{α : Type u_1}
[inst : NonUnitalNonAssocRing α]
(k : α)
(h : ∀ (x : α), k * x = 0 → x = 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 = 0 → x = 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 : α}
:
def
NoZeroDivisors.toCancelMonoidWithZero
{α : Type u_1}
[inst : Ring α]
[inst : NoZeroDivisors α]
:
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
def
NoZeroDivisors.toCancelCommMonoidWithZero
{α : Type u_1}
[inst : CommRing α]
[inst : NoZeroDivisors α]
:
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
Equations
- IsDomain.toCancelMonoidWithZero = CancelMonoidWithZero.mk
instance
IsDomain.toCancelCommMonoidWithZero
{α : Type u_1}
[inst : CommSemiring α]
[inst : IsDomain α]
:
Equations
- IsDomain.toCancelCommMonoidWithZero = CancelCommMonoidWithZero.mk