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.

source

def non_zero_divisors (R : Type u_1) [monoid_with_zero R] :

submonoid R

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

Equations

R⁰ = {carrier := {x : R | ∀ (z : R), z * x = 0 → z = 0}, mul_mem' := _, one_mem' := _}

source

theorem mem_non_zero_divisors_iff {M : Type u_1} [monoid_with_zero M] {r : M} :

r ∈ M⁰ ↔ ∀ (x : M), x * r = 0 → x = 0

source

theorem mul_right_mem_non_zero_divisors_eq_zero_iff {M : Type u_1} [monoid_with_zero M] {x r : M} (hr : r ∈ M⁰) :

x * r = 0 ↔ x = 0

source

@[simp]

theorem mul_right_coe_non_zero_divisors_eq_zero_iff {M : Type u_1} [monoid_with_zero M] {x : M} {c : ↥M⁰} :

x * ↑c = 0 ↔ x = 0

source

theorem mul_left_mem_non_zero_divisors_eq_zero_iff {M₁ : Type u_3} [comm_monoid_with_zero M₁] {r x : M₁} (hr : r ∈ M₁⁰) :

r * x = 0 ↔ x = 0

source

@[simp]

theorem mul_left_coe_non_zero_divisors_eq_zero_iff {M₁ : Type u_3} [comm_monoid_with_zero M₁] {c : ↥M₁⁰} {x : M₁} :

(↑c) * x = 0 ↔ x = 0

source

theorem mul_cancel_right_mem_non_zero_divisor {R : Type u_4} [ring R] {x y r : R} (hr : r ∈ R⁰) :

x * r = y * r ↔ x = y

source

theorem mul_cancel_right_coe_non_zero_divisor {R : Type u_4} [ring R] {x y : R} {c : ↥R⁰} :

x * ↑c = y * ↑c ↔ x = y

source

@[simp]

theorem mul_cancel_left_mem_non_zero_divisor {R' : Type u_5} [comm_ring R'] {x y r : R'} (hr : r ∈ R'⁰) :

r * x = r * y ↔ x = y

source

theorem mul_cancel_left_coe_non_zero_divisor {R' : Type u_5} [comm_ring R'] {x y : R'} {c : ↥R'⁰} :

(↑c) * x = (↑c) * y ↔ x = y

source

theorem non_zero_divisors.ne_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] {x : M} (hx : x ∈ M⁰) :

x ≠ 0

source

theorem non_zero_divisors.coe_ne_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] (x : ↥M⁰) :

↑x ≠ 0

source

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₁⁰

source

theorem is_unit_of_mem_non_zero_divisors {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} (hx : x ∈ G₀⁰) :

is_unit x

source

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

source

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

source

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 ∈ M⁰

source

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

source

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 ∈ M⁰) :

⇑g x ≠ 0

source

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 ∈ M⁰) :

⇑g x ∈ M'⁰

source

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⁰

source

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) :

submonoid.powers a ≤ M⁰

source

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 ≤ M⁰) :

submonoid.map ↑f S ≤ M'⁰

source

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) :

M⁰ ≤ submonoid.comap ↑f M'⁰

source

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