Non-zero divisors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
The submonoid of non-zero-divisors of a monoid_with_zero R.
Equations
Instances for non_zero_divisors
theorem
mul_right_mem_non_zero_divisors_eq_zero_iff
{M : Type u_1}
[monoid_with_zero M]
{x r : M}
(hr : r ∈ non_zero_divisors M) :
@[simp]
theorem
mul_right_coe_non_zero_divisors_eq_zero_iff
{M : Type u_1}
[monoid_with_zero M]
{x : M}
{c : ↥(non_zero_divisors M)} :
theorem
mul_left_mem_non_zero_divisors_eq_zero_iff
{M₁ : Type u_3}
[comm_monoid_with_zero M₁]
{r x : M₁}
(hr : r ∈ non_zero_divisors M₁) :
@[simp]
theorem
mul_left_coe_non_zero_divisors_eq_zero_iff
{M₁ : Type u_3}
[comm_monoid_with_zero M₁]
{c : ↥(non_zero_divisors M₁)}
{x : M₁} :
theorem
non_zero_divisors.ne_zero
{M : Type u_1}
[monoid_with_zero M]
[nontrivial M]
{x : M}
(hx : x ∈ non_zero_divisors M) :
x ≠ 0
theorem
non_zero_divisors.coe_ne_zero
{M : Type u_1}
[monoid_with_zero M]
[nontrivial M]
(x : ↥(non_zero_divisors M)) :
theorem
mul_mem_non_zero_divisors
{M₁ : Type u_3}
[comm_monoid_with_zero M₁]
{a b : M₁} :
a * b ∈ non_zero_divisors M₁ ↔ a ∈ non_zero_divisors M₁ ∧ b ∈ non_zero_divisors M₁
theorem
is_unit_of_mem_non_zero_divisors
{G₀ : Type u_1}
[group_with_zero G₀]
{x : G₀}
(hx : x ∈ non_zero_divisors G₀) :
is_unit x
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_of_ne_zero
{M : Type u_1}
[monoid_with_zero M]
[no_zero_divisors M]
{x : M}
(hx : x ≠ 0) :
x ∈ non_zero_divisors M
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 ∈ non_zero_divisors 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]
[monoid_with_zero M']
[nontrivial M]
[zero_hom_class F M M']
(g : F)
(hg : function.injective ⇑g)
{x : M}
(h : x ∈ non_zero_divisors M) :
theorem
map_mem_non_zero_divisors
{M : Type u_1}
{M' : Type u_2}
{F : Type u_6}
[monoid_with_zero M]
[monoid_with_zero M']
[nontrivial M]
[no_zero_divisors M']
[zero_hom_class F M M']
(g : F)
(hg : function.injective ⇑g)
{x : M}
(h : x ∈ non_zero_divisors M) :
⇑g x ∈ non_zero_divisors M'
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 ≤ non_zero_divisors M
theorem
powers_le_non_zero_divisors_of_no_zero_divisors
{M : Type u_1}
[monoid_with_zero M]
[no_zero_divisors M]
{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]
[monoid_with_zero M']
[no_zero_divisors M']
[monoid_with_zero_hom_class F M M']
(f : F)
(hf : function.injective ⇑f)
{S : submonoid M}
(hS : S ≤ non_zero_divisors M) :
submonoid.map f S ≤ non_zero_divisors M'
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]
[monoid_with_zero M']
[no_zero_divisors M']
[monoid_with_zero_hom_class F M M']
(f : F)
(hf : function.injective ⇑f) :
theorem
prod_zero_iff_exists_zero
{M₁ : Type u_3}
[comm_monoid_with_zero M₁]
[no_zero_divisors M₁]
[nontrivial M₁]
{s : multiset M₁} :