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} :
x 0y * x = 0y = 0

theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {A : Type u_2} [integral_domain A] {x y : A} :
x 0x * y = 0y = 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} :