Non-zero divisors in a ring #
theorem
IsLeftRegular.pow_injective
{R : Type u_1}
[Monoid R]
{r : R}
[IsMulTorsionFree R]
(hx : IsLeftRegular r)
(hx' : r ≠ 1)
:
Function.Injective fun (n : ℕ) => r ^ n
theorem
IsAddLeftRegular.nsmul_injective
{R : Type u_1}
[AddMonoid R]
{r : R}
[IsAddTorsionFree R]
(hx : IsAddLeftRegular r)
(hx' : r ≠ 0)
:
Function.Injective fun (n : ℕ) => n • r
theorem
IsRightRegular.pow_injective
{M : Type u_2}
[Monoid M]
[IsMulTorsionFree M]
{x : M}
(hx : IsRightRegular x)
(hx' : x ≠ 1)
:
Function.Injective fun (n : ℕ) => x ^ n
theorem
IsAddRightRegular.nsmul_injective
{M : Type u_2}
[AddMonoid M]
[IsAddTorsionFree M]
{x : M}
(hx : IsAddRightRegular x)
(hx' : x ≠ 0)
:
Function.Injective fun (n : ℕ) => n • x
theorem
IsMulTorsionFree.pow_right_injective
{M : Type u_2}
[CancelMonoid M]
[IsMulTorsionFree M]
{x : M}
(hx : x ≠ 1)
:
Function.Injective fun (n : ℕ) => x ^ n
@[simp]
theorem
IsMulTorsionFree.pow_right_inj
{M : Type u_2}
[CancelMonoid M]
[IsMulTorsionFree M]
{x : M}
(hx : x ≠ 1)
{n m : ℕ}
:
x ^ n = x ^ m ↔ n = m
theorem
IsMulTorsionFree.pow_right_injective₀
{M : Type u_2}
[MonoidWithZero M]
[IsLeftCancelMulZero M]
[IsMulTorsionFree M]
{x : M}
(hx : x ≠ 1)
(hx' : x ≠ 0)
:
Function.Injective fun (n : ℕ) => x ^ n
@[simp]
theorem
IsMulTorsionFree.pow_right_inj₀
{M : Type u_2}
[MonoidWithZero M]
[IsLeftCancelMulZero M]
[IsMulTorsionFree M]
{x : M}
(hx : x ≠ 1)
(hx' : x ≠ 0)
{n m : ℕ}
:
x ^ n = x ^ m ↔ n = m
theorem
IsLeftRegular.isUnit_of_finite
{R : Type u_1}
[Monoid R]
{r : R}
[Finite R]
(h : IsLeftRegular r)
:
IsUnit r
theorem
IsRightRegular.isUnit_of_finite
{R : Type u_1}
[Monoid R]
{r : R}
[Finite R]
(h : IsRightRegular r)
:
IsUnit r
theorem
isLeftRegular_iff_mem_nonZeroDivisorsLeft
{R : Type u_1}
[Ring R]
{r : R}
:
IsLeftRegular r ↔ r ∈ nonZeroDivisorsLeft R
theorem
isRightRegular_iff_mem_nonZeroDivisorsRight
{R : Type u_1}
[Ring R]
{r : R}
:
IsRightRegular r ↔ r ∈ nonZeroDivisorsRight R
theorem
isRegular_iff_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
{r : R}
:
IsRegular r ↔ r ∈ nonZeroDivisors R
theorem
le_nonZeroDivisorsLeft_iff_isLeftRegular
{R : Type u_1}
[Ring R]
{S : Submonoid R}
:
S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular ↑s
theorem
le_nonZeroDivisorsRight_iff_isRightRegular
{R : Type u_1}
[Ring R]
{S : Submonoid R}
:
S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular ↑s
theorem
le_nonZeroDivisors_iff_isRegular
{R : Type u_1}
[Ring R]
{S : Submonoid R}
:
S ≤ nonZeroDivisors R ↔ ∀ (s : ↥S), IsRegular ↑s
theorem
mul_cancel_left_mem_nonZeroDivisorsLeft
{R : Type u_1}
[Ring R]
{x y r : R}
(hr : r ∈ nonZeroDivisorsLeft R)
:
r * x = r * y ↔ x = y
theorem
mul_cancel_right_mem_nonZeroDivisorsRight
{R : Type u_1}
[Ring R]
{x y r : R}
(hr : r ∈ nonZeroDivisorsRight R)
:
x * r = y * r ↔ x = y
@[simp]
theorem
mul_cancel_left_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y r : R}
(hr : r ∈ nonZeroDivisors R)
:
r * x = r * y ↔ x = y
theorem
mul_cancel_left_coe_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
↑c * x = ↑c * y ↔ x = y
theorem
mul_cancel_right_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y r : R}
(hr : r ∈ nonZeroDivisors R)
:
x * r = y * r ↔ x = y
theorem
mul_cancel_right_coe_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
x * ↑c = y * ↑c ↔ x = y
theorem
isUnit_iff_mem_nonZeroDivisors_of_finite
{R : Type u_1}
[Ring R]
{a : R}
[Finite R]
:
IsUnit a ↔ a ∈ nonZeroDivisors R
In a finite ring, an element is a unit iff it is a non-zero-divisor.
theorem
dvd_cancel_left_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y r : R}
(hr : r ∈ nonZeroDivisors R)
:
r * x ∣ r * y ↔ x ∣ y
theorem
dvd_cancel_left_coe_nonZeroDivisors
{R : Type u_1}
[Ring R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
↑c * x ∣ ↑c * y ↔ x ∣ y
theorem
dvd_cancel_right_mem_nonZeroDivisors
{R : Type u_1}
[CommRing R]
{r x y : R}
(hr : r ∈ nonZeroDivisors R)
:
x * r ∣ y * r ↔ x ∣ y
theorem
dvd_cancel_right_coe_nonZeroDivisors
{R : Type u_1}
[CommRing R]
{x y : R}
{c : ↥(nonZeroDivisors R)}
:
x * ↑c ∣ y * ↑c ↔ x ∣ y