Lemmas about regular elements in rings. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
is_left_regular_of_non_zero_divisor
{α : Type u_1}
[non_unital_non_assoc_ring α]
(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 no_zero_divisors.
theorem
is_right_regular_of_non_zero_divisor
{α : Type u_1}
[non_unital_non_assoc_ring α]
(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 no_zero_divisors.
theorem
is_regular_of_ne_zero'
{α : Type u_1}
[non_unital_non_assoc_ring α]
[no_zero_divisors α]
{k : α}
(hk : k ≠ 0) :
theorem
is_regular_iff_ne_zero'
{α : Type u_1}
[nontrivial α]
[non_unital_non_assoc_ring α]
[no_zero_divisors α]
{k : α} :
is_regular k ↔ k ≠ 0
@[reducible]
A ring with no zero divisors is a cancel_monoid_with_zero.
Note this is not an instance as it forms a typeclass loop.
Equations
- no_zero_divisors.to_cancel_monoid_with_zero = {mul := monoid_with_zero.mul (semiring.to_monoid_with_zero α), mul_assoc := _, one := monoid_with_zero.one (semiring.to_monoid_with_zero α), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (semiring.to_monoid_with_zero α), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (semiring.to_monoid_with_zero α), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
@[reducible]
def
no_zero_divisors.to_cancel_comm_monoid_with_zero
{α : Type u_1}
[comm_ring α]
[no_zero_divisors α] :
A commutative ring with no zero divisors is a cancel_comm_monoid_with_zero.
Note this is not an instance as it forms a typeclass loop.
Equations
- no_zero_divisors.to_cancel_comm_monoid_with_zero = {mul := cancel_monoid_with_zero.mul no_zero_divisors.to_cancel_monoid_with_zero, mul_assoc := _, one := cancel_monoid_with_zero.one no_zero_divisors.to_cancel_monoid_with_zero, one_mul := _, mul_one := _, npow := cancel_monoid_with_zero.npow no_zero_divisors.to_cancel_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := cancel_monoid_with_zero.zero no_zero_divisors.to_cancel_monoid_with_zero, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _}
@[protected, instance]
Equations
- is_domain.to_cancel_monoid_with_zero = {mul := monoid_with_zero.mul (semiring.to_monoid_with_zero α), mul_assoc := _, one := monoid_with_zero.one (semiring.to_monoid_with_zero α), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (semiring.to_monoid_with_zero α), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (semiring.to_monoid_with_zero α), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
@[protected, instance]
Equations
- is_domain.to_cancel_comm_monoid_with_zero = {mul := comm_semiring.mul _inst_1, mul_assoc := _, one := comm_semiring.one _inst_1, one_mul := _, mul_one := _, npow := comm_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_semiring.zero _inst_1, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _}