Non-zero divisors #

In this file we define the submonoid nonZeroDivisors of a MonoidWithZero.

Notations #

This file declares the notation R⁰ for the submonoid of non-zero-divisors of R, in the locale nonZeroDivisors.

Use the statement open nonZeroDivisors to access this notation in your own code.

source

ink

def nonZeroDivisors (R : Type u_1) [inst : MonoidWithZero R] :

Submonoid R

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

Equations

One or more equations did not get rendered due to their size.

source

ink

def nonZeroDivisors.«term_⁰» :

Lean.TrailingParserDescr

The notation for the submonoid of non-zerodivisors.

Equations

nonZeroDivisors.«term_⁰» = Lean.ParserDescr.trailingNode `nonZeroDivisors.term_⁰ 9000 0 (Lean.ParserDescr.symbol "⁰")

source

ink

theorem mem_nonZeroDivisors_iff {M : Type u_1} [inst : MonoidWithZero M] {r : M} :

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

source

ink

theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M : Type u_1} [inst : MonoidWithZero M] {x : M} {r : M} (hr : r ∈ nonZeroDivisors M) :

x * r = 0 ↔ x = 0

source

ink

@[simp]

theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M : Type u_1} [inst : MonoidWithZero M] {x : M} {c : { x // x ∈ nonZeroDivisors M }} :

x * ↑c = 0 ↔ x = 0

source

ink

theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₁ : Type u_1} [inst : CommMonoidWithZero M₁] {r : M₁} {x : M₁} (hr : r ∈ nonZeroDivisors M₁) :

r * x = 0 ↔ x = 0

source

ink

@[simp]

theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₁ : Type u_1} [inst : CommMonoidWithZero M₁] {c : { x // x ∈ nonZeroDivisors M₁ }} {x : M₁} :

↑c * x = 0 ↔ x = 0

source

ink

theorem mul_cancel_right_mem_nonZeroDivisors {R : Type u_1} [inst : Ring R] {x : R} {y : R} {r : R} (hr : r ∈ nonZeroDivisors R) :

x * r = y * r ↔ x = y

source

ink

theorem mul_cancel_right_coe_nonZeroDivisors {R : Type u_1} [inst : Ring R] {x : R} {y : R} {c : { x // x ∈ nonZeroDivisors R }} :

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

source

ink

@[simp]

theorem mul_cancel_left_mem_nonZeroDivisors {R' : Type u_1} [inst : CommRing R'] {x : R'} {y : R'} {r : R'} (hr : r ∈ nonZeroDivisors R') :

r * x = r * y ↔ x = y

source

ink

theorem mul_cancel_left_coe_nonZeroDivisors {R' : Type u_1} [inst : CommRing R'] {x : R'} {y : R'} {c : { x // x ∈ nonZeroDivisors R' }} :

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

source

ink

theorem nonZeroDivisors.ne_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : Nontrivial M] {x : M} (hx : x ∈ nonZeroDivisors M) :

x ≠ 0

source

ink

theorem nonZeroDivisors.coe_ne_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : Nontrivial M] (x : { x // x ∈ nonZeroDivisors M }) :

↑x ≠ 0

source

ink

theorem mul_mem_nonZeroDivisors {M₁ : Type u_1} [inst : CommMonoidWithZero M₁] {a : M₁} {b : M₁} :

a * b ∈ nonZeroDivisors M₁ ↔ a ∈ nonZeroDivisors M₁ ∧ b ∈ nonZeroDivisors M₁

source

ink

theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type u_1} [inst : GroupWithZero G₀] {x : G₀} (hx : x ∈ nonZeroDivisors G₀) :

IsUnit x

source

ink

theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {x : M} {y : M} (hnx : x ≠ 0) (hxy : y * x = 0) :

y = 0

source

ink

theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {x : M} {y : M} (hnx : x ≠ 0) (hxy : x * y = 0) :

y = 0

source

ink

theorem mem_nonZeroDivisors_of_ne_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {x : M} (hx : x ≠ 0) :

x ∈ nonZeroDivisors M

source

ink

theorem mem_nonZeroDivisors_iff_ne_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] [inst : Nontrivial M] {x : M} :

x ∈ nonZeroDivisors M ↔ x ≠ 0

source

ink

theorem map_ne_zero_of_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_3} {F : Type u_2} [inst : MonoidWithZero M] [inst : MonoidWithZero M'] [inst : Nontrivial M] [inst : ZeroHomClass F M M'] (g : F) (hg : Function.Injective ↑g) {x : M} (h : x ∈ nonZeroDivisors M) :

↑g x ≠ 0

source

ink

theorem map_mem_nonZeroDivisors {M : Type u_1} {M' : Type u_2} {F : Type u_3} [inst : MonoidWithZero M] [inst : MonoidWithZero M'] [inst : Nontrivial M] [inst : NoZeroDivisors M'] [inst : ZeroHomClass F M M'] (g : F) (hg : Function.Injective ↑g) {x : M} (h : x ∈ nonZeroDivisors M) :

↑g x ∈ nonZeroDivisors M'

source

ink

theorem le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {S : Submonoid M} (hS : ¬0 ∈ S) :

S ≤ nonZeroDivisors M

source

ink

theorem powers_le_nonZeroDivisors_of_noZeroDivisors {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {a : M} (ha : a ≠ 0) :

Submonoid.powers a ≤ nonZeroDivisors M

source

ink

theorem map_le_nonZeroDivisors_of_injective {M : Type u_3} {M' : Type u_1} {F : Type u_2} [inst : MonoidWithZero M] [inst : MonoidWithZero M'] [inst : NoZeroDivisors M'] [inst : MonoidWithZeroHomClass F M M'] (f : F) (hf : Function.Injective ↑f) {S : Submonoid M} (hS : S ≤ nonZeroDivisors M) :

Submonoid.map f S ≤ nonZeroDivisors M'

source

ink

theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective {M : Type u_3} {M' : Type u_1} {F : Type u_2} [inst : MonoidWithZero M] [inst : MonoidWithZero M'] [inst : NoZeroDivisors M'] [inst : MonoidWithZeroHomClass F M M'] (f : F) (hf : Function.Injective ↑f) :

nonZeroDivisors M ≤ Submonoid.comap f (nonZeroDivisors M')

source

ink

theorem prod_zero_iff_exists_zero {M₁ : Type u_1} [inst : CommMonoidWithZero M₁] [inst : NoZeroDivisors M₁] [inst : Nontrivial M₁] {s : Multiset M₁} :

Multiset.prod s = 0 ↔ ∃ r x, r = 0