# Non-zero divisors and smul-divisors #

In this file we define the submonoid nonZeroDivisors and nonZeroSMulDivisors of a MonoidWithZero. We also define nonZeroDivisorsLeft and nonZeroDivisorsRight for non-commutative monoids.

## Notations #

This file declares the notations:

• R⁰ for the submonoid of non-zero-divisors of R, in the locale nonZeroDivisors.
• R⁰[M] for the submonoid of non-zero smul-divisors of R with respect to M, in the locale nonZeroSMulDivisors

Use the statement open scoped nonZeroDivisors nonZeroSMulDivisors to access this notation in your own code.

def nonZeroDivisorsLeft (M₀ : Type u_1) [] :

The collection of elements of a MonoidWithZero that are not left zero divisors form a Submonoid.

Equations
• = { carrier := {x : M₀ | ∀ (y : M₀), y * x = 0y = 0}, mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [] {x : M₀} :
∀ (y : M₀), y * x = 0y = 0
theorem nmem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [] {r : M₀} :
r {s : M₀ | s * r = 0 s 0}.Nonempty
def nonZeroDivisorsRight (M₀ : Type u_1) [] :

The collection of elements of a MonoidWithZero that are not right zero divisors form a Submonoid.

Equations
• = { carrier := {x : M₀ | ∀ (y : M₀), x * y = 0y = 0}, mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [] {x : M₀} :
∀ (y : M₀), x * y = 0y = 0
theorem nmem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [] {r : M₀} :
r {s : M₀ | r * s = 0 s 0}.Nonempty
theorem nonZeroDivisorsLeft_eq_right (M₀ : Type u_2) [] :
@[simp]
theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [] [] [] :
() = {x : M₀ | x 0}
@[simp]
theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [] [] [] :
() = {x : M₀ | x 0}
def nonZeroDivisors (R : Type u_2) [] :

The submonoid of non-zero-divisors of a MonoidWithZero R.

Equations
• = { carrier := {x : R | ∀ (z : R), z * x = 0z = 0}, mul_mem' := , one_mem' := }
Instances For

The notation for the submonoid of non-zerodivisors.

Equations
Instances For
def nonZeroSMulDivisors (R : Type u_2) [] (M : Type u_3) [Zero M] [] :

Let R be a monoid with zero and M an additive monoid with an R-action, then the collection of non-zero smul-divisors forms a submonoid. These elements are also called M-regular.

Equations
• = { carrier := {r : R | ∀ (m : M), r m = 0m = 0}, mul_mem' := , one_mem' := }
Instances For

The notation for the submonoid of non-zero smul-divisors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem mem_nonZeroDivisors_iff {M : Type u_2} [] {r : M} :
∀ (x : M), x * r = 0x = 0
theorem nmem_nonZeroDivisors_iff {M : Type u_2} [] {r : M} :
r {s : M | s * r = 0 s 0}.Nonempty
theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_2} [] {x : M} {r : M} (hr : ) :
x * r = 0 x = 0
@[simp]
theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M : Type u_2} [] {x : M} {c : ()} :
x * c = 0 x = 0
theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_4} [] {r : M₁} {x : M₁} (hr : r ) :
r * x = 0 x = 0
@[simp]
theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₁ : Type u_4} [] {c : ()} {x : M₁} :
c * x = 0 x = 0
theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_5} [Ring R] {x : R} {y : R} {r : R} (hr : ) :
x * r = y * r x = y
theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_5} [Ring R] {x : R} {y : R} {c : ()} :
x * c = y * c x = y
@[simp]
theorem mul_cancel_left_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ) :
r * x = r * y x = y
theorem mul_cancel_left_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : ()} :
c * x = c * y x = y
theorem dvd_cancel_right_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ) :
x * r y * r x y
theorem dvd_cancel_right_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : ()} :
x * c y * c x y
theorem dvd_cancel_left_mem_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ) :
r * x r * y x y
theorem dvd_cancel_left_coe_nonZeroDivisors {R' : Type u_6} [CommRing R'] {x : R'} {y : R'} {c : ()} :
c * x c * y x y
theorem zero_not_mem_nonZeroDivisors {M : Type u_2} [] [] :
0
theorem nonZeroDivisors.ne_zero {M : Type u_2} [] [] {x : M} (hx : ) :
x 0
@[simp]
theorem nonZeroDivisors.coe_ne_zero {M : Type u_2} [] [] (x : ()) :
x 0
theorem mul_mem_nonZeroDivisors {M₁ : Type u_4} [] {a : M₁} {b : M₁} :
a * b a b
theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_8} [] {x : G₀} (hx : x ) :
theorem IsUnit.mem_nonZeroDivisors {M : Type u_2} [] {a : M} (ha : ) :
theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_2} [] [] {x : M} {y : M} (hnx : x 0) (hxy : y * x = 0) :
y = 0
theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {M : Type u_2} [] [] {x : M} {y : M} (hnx : x 0) (hxy : x * y = 0) :
y = 0
theorem mem_nonZeroDivisors_of_ne_zero {M : Type u_2} [] [] {x : M} (hx : x 0) :
theorem mem_nonZeroDivisors_iff_ne_zero {M : Type u_2} [] [] [] {x : M} :
x 0
theorem map_ne_zero_of_mem_nonZeroDivisors {M : Type u_2} {M' : Type u_3} {F : Type u_7} [] [] [FunLike F M M'] [] [ZeroHomClass F M M'] (g : F) (hg : ) {x : M} (h : ) :
g x 0
theorem map_mem_nonZeroDivisors {M : Type u_2} {M' : Type u_3} {F : Type u_7} [] [] [FunLike F M M'] [] [] [ZeroHomClass F M M'] (g : F) (hg : ) {x : M} (h : ) :
g x
theorem le_nonZeroDivisors_of_noZeroDivisors {M : Type u_2} [] [] {S : } (hS : 0S) :
theorem powers_le_nonZeroDivisors_of_noZeroDivisors {M : Type u_2} [] [] {a : M} (ha : a 0) :
theorem map_le_nonZeroDivisors_of_injective {M : Type u_2} {M' : Type u_3} {F : Type u_7} [] [] [FunLike F M M'] [] [] (f : F) (hf : ) {S : } (hS : ) :
theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective {M : Type u_2} {M' : Type u_3} {F : Type u_7} [] [] [FunLike F M M'] [] [] (f : F) (hf : ) :
theorem isUnit_iff_mem_nonZeroDivisors_of_finite {R : Type u_5} [Ring R] [] {a : R} :

In a finite ring, an element is a unit iff it is a non-zero-divisor.

theorem mem_nonZeroSMulDivisors_iff {R : Type u_2} {M : Type u_3} [] [Zero M] [] {x : R} :
x ∀ (m : M), x m = 0m = 0

The non-zero •-divisors with • as right multiplication correspond with the non-zero divisors. Note that the MulOpposite is needed because we defined nonZeroDivisors with multiplication on the right.

@[simp]
theorem val_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [] (u : M₀ˣ) :
(unitsNonZeroDivisorsEquiv.symm u) = u
@[simp]
theorem val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [] (u : M₀ˣ) :
(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = u⁻¹
@[simp]
theorem unitsNonZeroDivisorsEquiv_apply {M₀ : Type u_1} [] :
∀ (a : (())ˣ), unitsNonZeroDivisorsEquiv a = ((Units.map ().subtype)).toFun a
def unitsNonZeroDivisorsEquiv {M₀ : Type u_1} [] :
(())ˣ ≃* M₀ˣ

The units of the monoid of non-zero divisors of M₀ are equivalent to the units of M₀.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem nonZeroDivisors.associated_coe {M₀ : Type u_1} [] {a : ()} {b : ()} :
Associated a b
theorem mk_mem_nonZeroDivisors_associates {M₀ : Type u_2} [] {a : M₀} :
a
def associatesNonZeroDivisorsEquiv {M₀ : Type u_2} [] :
() ≃*

The non-zero divisors of associates of a monoid with zero M₀ are isomorphic to the associates of the non-zero divisors of M₀ under the map ⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem associatesNonZeroDivisorsEquiv_mk_mk {M₀ : Type u_2} [] (a : M₀) (ha : a ) :
associatesNonZeroDivisorsEquiv a, ha = a,
@[simp]
theorem associatesNonZeroDivisorsEquiv_symm_mk_mk {M₀ : Type u_2} [] (a : M₀) (ha : a ) :
associatesNonZeroDivisorsEquiv.symm a, ha = a,