mathlib documentation

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) [monoid_with_zero R] :

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

Equations
theorem non_zero_divisors.ne_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] {x : M} (hx : x M) :
x 0
theorem non_zero_divisors.coe_ne_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] (x : M) :
x 0
theorem mul_mem_non_zero_divisors {M₁ : Type u_3} [comm_monoid_with_zero M₁] {a b : M₁} :
a * b M₁ a M₁ b M₁
theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} [monoid_with_zero M] [no_zero_divisors M] {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} [monoid_with_zero M] [no_zero_divisors M] {x y : M} (hnx : x 0) (hxy : x * y = 0) :
y = 0
theorem mem_non_zero_divisors_iff_ne_zero {M : Type u_1} [monoid_with_zero M] [no_zero_divisors M] [nontrivial M] {x : M} :
x M x 0
theorem monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors {M : Type u_1} {M' : Type u_2} [monoid_with_zero M] [monoid_with_zero M'] [nontrivial M] (g : monoid_with_zero_hom M M') (hg : function.injective g) {x : M} (h : x M) :
g x 0
theorem ring_hom.map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} {R' : Type u_2} [semiring R] [semiring R'] [nontrivial R] (g : R →+* R') (hg : function.injective g) {x : R} (h : x R) :
g x 0
theorem monoid_with_zero_hom.map_mem_non_zero_divisors {M : Type u_1} {M' : Type u_2} [monoid_with_zero M] [monoid_with_zero M'] [nontrivial M] [no_zero_divisors M'] (g : monoid_with_zero_hom M M') (hg : function.injective g) {x : M} (h : x M) :
g x M'
theorem ring_hom.map_mem_non_zero_divisors {R : Type u_1} {R' : Type u_2} [semiring R] [semiring R'] [nontrivial R] [no_zero_divisors R'] (g : R →+* R') (hg : function.injective g) {x : R} (h : x R) :
g x R'
theorem le_non_zero_divisors_of_no_zero_divisors {M : Type u_1} [monoid_with_zero M] [no_zero_divisors M] {S : submonoid M} (hS : 0 S) :
S M
theorem ring_hom.map_le_non_zero_divisors_of_injective {R : Type u_1} {R' : Type u_2} [semiring R] [semiring R'] [nontrivial R] [no_zero_divisors R'] (f : R →+* R') (hf : function.injective f) {S : submonoid R} (hS : S R) :
theorem prod_zero_iff_exists_zero {M₁ : Type u_3} [comm_monoid_with_zero M₁] [no_zero_divisors M₁] [nontrivial M₁] {s : multiset M₁} :
s.prod = 0 ∃ (r : M₁) (hr : r s), r = 0