Non-zero divisors
In this file we define the submonoid non_zero_divisors of a monoid_with_zero.
The submonoid of non-zero-divisors of a monoid_with_zero R.
theorem
mul_mem_non_zero_divisors
{R : Type u_1}
[comm_ring R]
{a b : R} :
a * b ∈ non_zero_divisors R ↔ a ∈ non_zero_divisors R ∧ b ∈ non_zero_divisors R
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} :
x ∈ non_zero_divisors A ↔ x ≠ 0
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)} :
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)} :
⇑g ↑x ∈ non_zero_divisors B
theorem
le_non_zero_divisors_of_domain
{A : Type u_2}
[integral_domain A]
{M : submonoid A}
(hM : ↑0 ∉ M) :
M ≤ non_zero_divisors A