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.

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 eq_zero_of_ne_zero_of_mul_right_eq_zero {A : Type u_2} [integral_domain A] {x y : A} (hnx : x 0) (hxy : y * x = 0) :
y = 0
theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {A : Type u_2} [integral_domain A] {x y : A} (hnx : x 0) (hxy : x * y = 0) :
y = 0
theorem mem_non_zero_divisors_iff_ne_zero {A : Type u_2} [integral_domain A] {x : A} :
theorem map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] [nontrivial R] {B : Type u_2} [ring B] {g : R →+* B} (hg : function.injective g) {x : (non_zero_divisors R)} :
g x 0
theorem map_mem_non_zero_divisors {A : Type u_2} [integral_domain A] {B : Type u_1} [integral_domain B] {g : A →+* B} (hg : function.injective g) {x : (non_zero_divisors A)} :
theorem le_non_zero_divisors_of_domain {A : Type u_2} [integral_domain A] {M : submonoid A} (hM : 0 M) :
theorem prod_zero_iff_exists_zero {R : Type u_1} [comm_semiring R] [no_zero_divisors R] [nontrivial R] {s : multiset R} :
s.prod = 0 ∃ (r : R) (hr : r s), r = 0