# Documentation

Mathlib.RingTheory.NonZeroDivisors

# Non-zero divisors #

In this file we define the submonoid nonZeroDivisors of a MonoidWithZero.

## Notations #

This file declares the notation R⁰ for the submonoid of non-zero-divisors of R, in the locale nonZeroDivisors.

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

def nonZeroDivisors (R : Type u_1) [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.

The notation for the submonoid of non-zerodivisors.

Equations
theorem mem_nonZeroDivisors_iff {M : Type u_1} [inst : ] {r : M} :
∀ (x : M), x * r = 0x = 0
theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_1} [inst : ] {x : M} {r : M} (hr : ) :
x * r = 0 x = 0
@[simp]
theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M : Type u_1} [inst : ] {x : M} {c : { x // }} :
x * c = 0 x = 0
theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_1} [inst : ] {r : M₁} {x : M₁} (hr : r ) :
r * x = 0 x = 0
@[simp]
theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₁ : Type u_1} [inst : ] {c : { x // x }} {x : M₁} :
c * x = 0 x = 0
theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_1} [inst : Ring R] {x : R} {y : R} {r : R} (hr : ) :
x * r = y * r x = y
theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_1} [inst : Ring R] {x : R} {y : R} {c : { x // }} :
x * c = y * c x = y
@[simp]
theorem mul_cancel_left_mem_nonZeroDivisors {R' : Type u_1} [inst : 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_1} [inst : CommRing R'] {x : R'} {y : R'} {c : { x // x }} :
c * x = c * y x = y
theorem nonZeroDivisors.ne_zero {M : Type u_1} [inst : ] [inst : ] {x : M} (hx : ) :
x 0
theorem nonZeroDivisors.coe_ne_zero {M : Type u_1} [inst : ] [inst : ] (x : { x // }) :
x 0
theorem mul_mem_nonZeroDivisors {M₁ : Type u_1} [inst : ] {a : M₁} {b : M₁} :
a * b a b
theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_1} [inst : ] {x : G₀} (hx : x ) :
theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} [inst : ] [inst : ] {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_1} [inst : ] [inst : ] {x : M} {y : M} (hnx : x 0) (hxy : x * y = 0) :
y = 0
theorem mem_nonZeroDivisors_of_ne_zero {M : Type u_1} [inst : ] [inst : ] {x : M} (hx : x 0) :
theorem mem_nonZeroDivisors_iff_ne_zero {M : Type u_1} [inst : ] [inst : ] [inst : ] {x : M} :
x 0
theorem map_ne_zero_of_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_3} {F : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ZeroHomClass F M M'] (g : F) (hg : ) {x : M} (h : ) :
g x 0
theorem map_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_2} {F : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ZeroHomClass F M M'] (g : F) (hg : ) {x : M} (h : ) :
g x
theorem le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [inst : ] [inst : ] {S : } (hS : ¬0 S) :
theorem powers_le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [inst : ] [inst : ] {a : M} (ha : a 0) :
theorem map_le_nonZeroDivisors_of_injective {M : Type u_3} {M' : Type u_1} {F : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : F) (hf : ) {S : } (hS : ) :
theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective {M : Type u_3} {M' : Type u_1} {F : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (f : F) (hf : ) :
theorem prod_zero_iff_exists_zero {M₁ : Type u_1} [inst : ] [inst : ] [inst : ] {s : Multiset M₁} :
r x, r = 0