# mathlibdocumentation

ring_theory.non_zero_divisors

# Non-zero divisors #

In this file we define the submonoid non_zero_divisors of a monoid_with_zero.

## Notations #

This file declares the notation R⁰ for the submonoid of non-zero-divisors of R, in the locale non_zero_divisors. Use the statement open_locale non_zero_divisors to access this notation in your own code.

def non_zero_divisors (R : Type u_1)  :

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

Equations
Instances for non_zero_divisors
theorem mem_non_zero_divisors_iff {M : Type u_1} {r : M} :
∀ (x : M), x * r = 0x = 0
theorem mul_right_mem_non_zero_divisors_eq_zero_iff {M : Type u_1} {x r : M} (hr : r ) :
x * r = 0 x = 0
@[simp]
theorem mul_right_coe_non_zero_divisors_eq_zero_iff {M : Type u_1} {x : M} {c : } :
x * c = 0 x = 0
theorem mul_left_mem_non_zero_divisors_eq_zero_iff {M₁ : Type u_3} {r x : M₁} (hr : r ) :
r * x = 0 x = 0
@[simp]
theorem mul_left_coe_non_zero_divisors_eq_zero_iff {M₁ : Type u_3} {c : } {x : M₁} :
c * x = 0 x = 0
theorem mul_cancel_right_mem_non_zero_divisor {R : Type u_4} [ring R] {x y r : R} (hr : r ) :
x * r = y * r x = y
theorem mul_cancel_right_coe_non_zero_divisor {R : Type u_4} [ring R] {x y : R} {c : } :
x * c = y * c x = y
@[simp]
theorem mul_cancel_left_mem_non_zero_divisor {R' : Type u_5} [comm_ring R'] {x y r : R'} (hr : r ) :
r * x = r * y x = y
theorem mul_cancel_left_coe_non_zero_divisor {R' : Type u_5} [comm_ring R'] {x y : R'} {c : } :
c * x = c * y x = y
theorem non_zero_divisors.ne_zero {M : Type u_1} [nontrivial M] {x : M} (hx : x ) :
x 0
theorem non_zero_divisors.coe_ne_zero {M : Type u_1} [nontrivial M] (x : ) :
x 0
theorem mul_mem_non_zero_divisors {M₁ : Type u_3} {a b : M₁} :
a * b
theorem is_unit_of_mem_non_zero_divisors {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} (hx : x ) :
theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} {x 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} {x y : M} (hnx : x 0) (hxy : x * y = 0) :
y = 0
theorem mem_non_zero_divisors_of_ne_zero {M : Type u_1} {x : M} (hx : x 0) :
theorem mem_non_zero_divisors_iff_ne_zero {M : Type u_1} [nontrivial M] {x : M} :
x 0
theorem map_ne_zero_of_mem_non_zero_divisors {M : Type u_1} {M' : Type u_2} {F : Type u_6} [monoid_with_zero M'] [nontrivial M] [ M'] (g : F) (hg : function.injective g) {x : M} (h : x ) :
g x 0
theorem map_mem_non_zero_divisors {M : Type u_1} {M' : Type u_2} {F : Type u_6} [monoid_with_zero M'] [nontrivial M] [no_zero_divisors M'] [ M'] (g : F) (hg : function.injective g) {x : M} (h : x ) :
g x
theorem le_non_zero_divisors_of_no_zero_divisors {M : Type u_1} {S : submonoid M} (hS : 0 S) :
theorem powers_le_non_zero_divisors_of_no_zero_divisors {M : Type u_1} {a : M} (ha : a 0) :
theorem map_le_non_zero_divisors_of_injective {M : Type u_1} {M' : Type u_2} {F : Type u_6} [monoid_with_zero M'] [no_zero_divisors M'] [ M'] (f : F) (hf : function.injective f) {S : submonoid M} (hS : S ) :
theorem non_zero_divisors_le_comap_non_zero_divisors_of_injective {M : Type u_1} {M' : Type u_2} {F : Type u_6} [monoid_with_zero M'] [no_zero_divisors M'] [ M'] (f : F) (hf : function.injective f) :
theorem prod_zero_iff_exists_zero {M₁ : Type u_3} [no_zero_divisors M₁] [nontrivial M₁] {s : multiset M₁} :
s.prod = 0 ∃ (r : M₁) (hr : r s), r = 0