Non-zero divisors in a ring #
theorem
IsLeftRegular.mem_nonZeroDivisorsLeft
{R : Type u_1}
[MonoidWithZero R]
{r : R}
(h : IsLeftRegular r)
:
theorem
IsRightRegular.mem_nonZeroDivisorsRight
{R : Type u_1}
[MonoidWithZero R]
{r : R}
(h : IsRightRegular r)
:
theorem
IsLeftRegular.isUnit_of_finite
{R : Type u_1}
[Monoid R]
[Finite R]
{r : R}
(h : IsLeftRegular r)
:
IsUnit r
theorem
IsRightRegular.isUnit_of_finite
{R : Type u_1}
[Monoid R]
[Finite R]
{r : R}
(h : IsRightRegular r)
:
IsUnit r
theorem
mul_cancel_right_coe_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
@[deprecated isLeftRegular_iff_mem_nonZeroDivisorsLeft (since := "2025-07-16")]
@[deprecated isRightRegular_iff_mem_nonZeroDivisorsRight (since := "2025-07-16")]
@[deprecated le_nonZeroDivisorsRight_iff_isRightRegular (since := "2025-07-16")]
In a finite ring, an element is a unit iff it is a non-zero-divisor.
theorem
mul_cancel_left_coe_nonZeroDivisors
{R : Type u_1}
[CommRing R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
theorem
dvd_cancel_right_coe_nonZeroDivisors
{R : Type u_1}
[CommRing R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
theorem
dvd_cancel_left_coe_nonZeroDivisors
{R : Type u_1}
[CommRing R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
: