Non-zero divisors and smul-divisors

In this file we define the submonoid nonZeroDivisors and nonZeroSMulDivisors of a MonoidWithZero. We also define nonZeroDivisorsLeft and nonZeroDivisorsRight for non-commutative monoids.

Notations

This file declares the notations:

• M₀⁰ for the submonoid of non-zero-divisors of M₀, in the locale nonZeroDivisors.
• M₀⁰[M] for the submonoid of non-zero smul-divisors of M₀ with respect to M, in the locale nonZeroSMulDivisors

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

def nonZeroDivisorsLeft (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀

The collection of elements of a MonoidWithZero that are not left zero divisors form a Submonoid.

Equations

• nonZeroDivisorsLeft M₀ = { carrier := {x : M₀ | ∀ (y : M₀), y * x = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem mem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ (y : M₀), y * x = 0 → y = 0

theorem notMem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∉ nonZeroDivisorsLeft M₀ ↔ {y : M₀ | y * x = 0 ∧ y ≠ 0}.Nonempty

@[deprecated notMem_nonZeroDivisorsLeft_iff (since := "2025-05-24")]

theorem nmem_nonZeroDivisorsLeft_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∉ nonZeroDivisorsLeft M₀ ↔ {y : M₀ | y * x = 0 ∧ y ≠ 0}.Nonempty

Alias of notMem_nonZeroDivisorsLeft_iff.

def nonZeroDivisorsRight (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀

The collection of elements of a MonoidWithZero that are not right zero divisors form a Submonoid.

Equations

• nonZeroDivisorsRight M₀ = { carrier := {x : M₀ | ∀ (y : M₀), x * y = 0 → y = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem mem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∈ nonZeroDivisorsRight M₀ ↔ ∀ (y : M₀), x * y = 0 → y = 0

theorem notMem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∉ nonZeroDivisorsRight M₀ ↔ {y : M₀ | x * y = 0 ∧ y ≠ 0}.Nonempty

@[deprecated notMem_nonZeroDivisorsRight_iff (since := "2025-05-24")]

theorem nmem_nonZeroDivisorsRight_iff (M₀ : Type u_1) [MonoidWithZero M₀] {x : M₀} : x ∉ nonZeroDivisorsRight M₀ ↔ {y : M₀ | x * y = 0 ∧ y ≠ 0}.Nonempty

Alias of notMem_nonZeroDivisorsRight_iff.

theorem nonZeroDivisorsLeft_eq_right (M₀ : Type u_2) [CommMonoidWithZero M₀] : nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀

@[simp]

theorem coe_nonZeroDivisorsLeft_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsLeft M₀) = {x : M₀ | x ≠ 0}

@[simp]

theorem coe_nonZeroDivisorsRight_eq (M₀ : Type u_1) [MonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] : ↑(nonZeroDivisorsRight M₀) = {x : M₀ | x ≠ 0}

def nonZeroDivisors (M₀ : Type u_1) [MonoidWithZero M₀] : Submonoid M₀

The submonoid of non-zero-divisors of a MonoidWithZero M₀.

Equations

• nonZeroDivisors M₀ = { carrier := {x : M₀ | ∀ (z : M₀), z * x = 0 → z = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

def nonZeroDivisors.«term_⁰» : Lean.TrailingParserDescr

The notation for the submonoid of non-zero divisors.

Equations

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

def nonZeroSMulDivisors (M₀ : Type u_1) [MonoidWithZero M₀] (M : Type u_2) [Zero M] [MulAction M₀ M] : Submonoid M₀

Let M₀ be a monoid with zero and M an additive monoid with an M₀-action, then the collection of non-zero smul-divisors forms a submonoid.

These elements are also called M-regular.

Equations

• nonZeroSMulDivisors M₀ M = { carrier := {r : M₀ | ∀ (m : M), r • m = 0 → m = 0}, mul_mem' := ⋯, one_mem' := ⋯ }

def nonZeroSMulDivisors.«term_⁰[_]» : Lean.TrailingParserDescr

The notation for the submonoid of non-zero smul-divisors.

Equations

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

theorem nonZeroDivisorsLeft_eq_nonZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] : nonZeroDivisorsLeft M₀ = nonZeroDivisors M₀

theorem nonZeroDivisorsRight_eq_nonZeroSMulDivisors {M₀ : Type u_2} [MonoidWithZero M₀] : nonZeroDivisorsRight M₀ = nonZeroSMulDivisors M₀ M₀

theorem mem_nonZeroDivisors_iff {M₀ : Type u_2} [MonoidWithZero M₀] {r : M₀} : r ∈ nonZeroDivisors M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0

theorem notMem_nonZeroDivisors_iff {M₀ : Type u_2} [MonoidWithZero M₀] {r : M₀} : r ∉ nonZeroDivisors M₀ ↔ {s : M₀ | s * r = 0 ∧ s ≠ 0}.Nonempty

@[deprecated notMem_nonZeroDivisors_iff (since := "2025-05-24")]

theorem nmem_nonZeroDivisors_iff {M₀ : Type u_2} [MonoidWithZero M₀] {r : M₀} : r ∉ nonZeroDivisors M₀ ↔ {s : M₀ | s * r = 0 ∧ s ≠ 0}.Nonempty

Alias of notMem_nonZeroDivisors_iff.

theorem mul_right_mem_nonZeroDivisors_eq_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] {r x : M₀} (hr : r ∈ nonZeroDivisors M₀) : x * r = 0 ↔ x = 0

@[simp]

theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} {c : ↥(nonZeroDivisors M₀)} : x * ↑c = 0 ↔ x = 0

theorem IsUnit.mem_nonZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} (hx : IsUnit x) : x ∈ nonZeroDivisors M₀

theorem zero_notMem_nonZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] : 0 ∉ nonZeroDivisors M₀

@[deprecated zero_notMem_nonZeroDivisors (since := "2025-05-23")]

theorem zero_not_mem_nonZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] : 0 ∉ nonZeroDivisors M₀

Alias of zero_notMem_nonZeroDivisors.

theorem nonZeroDivisors.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [Nontrivial M₀] (hx : x ∈ nonZeroDivisors M₀) : x ≠ 0

@[simp]

theorem nonZeroDivisors.coe_ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] (x : ↥(nonZeroDivisors M₀)) : ↑x ≠ 0

instance instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] [IsLeftCancelMulZero M₀] : LeftCancelMonoid ↥(nonZeroDivisors M₀)

Equations

• instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero = { toMonoid := (nonZeroDivisors M₀).toMonoid, mul_left_cancel := ⋯ }

instance instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] [IsRightCancelMulZero M₀] : RightCancelMonoid ↥(nonZeroDivisors M₀)

Equations

• instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero = { toMonoid := (nonZeroDivisors M₀).toMonoid, mul_right_cancel := ⋯ }

theorem eq_zero_of_ne_zero_of_mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) (hxy : y * x = 0) : y = 0

theorem eq_zero_of_ne_zero_of_mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) (hxy : x * y = 0) : y = 0

theorem mem_nonZeroDivisors_of_ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) : x ∈ nonZeroDivisors M₀

@[simp]

theorem mem_nonZeroDivisors_iff_ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] [Nontrivial M₀] : x ∈ nonZeroDivisors M₀ ↔ x ≠ 0

theorem le_nonZeroDivisors_of_noZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] [NoZeroDivisors M₀] {S : Submonoid M₀} (hS : 0 ∉ S) : S ≤ nonZeroDivisors M₀

theorem powers_le_nonZeroDivisors_of_noZeroDivisors {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] (hx : x ≠ 0) : Submonoid.powers x ≤ nonZeroDivisors M₀

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

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

theorem MulEquivClass.map_nonZeroDivisors {M₀ : Type u_4} {S : Type u_5} {F : Type u_6} [MonoidWithZero M₀] [MonoidWithZero S] [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) : Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S

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

theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Function.Injective ⇑f) : nonZeroDivisors M₀ ≤ Submonoid.comap f (nonZeroDivisors M₀')

theorem mem_nonZeroDivisors_of_injective {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] {x : M₀} [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Function.Injective ⇑f) (hx : f x ∈ nonZeroDivisors M₀') : x ∈ nonZeroDivisors M₀

If an element maps to a non-zero-divisor via injective homomorphism, then it is a non-zero-divisor.

@[deprecated mem_nonZeroDivisors_of_injective (since := "2025-02-03")]

theorem mem_nonZeroDivisor_of_injective {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] {x : M₀} [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Function.Injective ⇑f) (hx : f x ∈ nonZeroDivisors M₀') : x ∈ nonZeroDivisors M₀

Alias of mem_nonZeroDivisors_of_injective.

---

If an element maps to a non-zero-divisor via injective homomorphism, then it is a non-zero-divisor.

theorem comap_nonZeroDivisors_le_of_injective {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Function.Injective ⇑f) : Submonoid.comap f (nonZeroDivisors M₀') ≤ nonZeroDivisors M₀

@[deprecated comap_nonZeroDivisors_le_of_injective (since := "2025-02-03")]

theorem comap_nonZeroDivisor_le_of_injective {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [MonoidWithZero M₀] [MonoidWithZero M₀'] [FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Function.Injective ⇑f) : Submonoid.comap f (nonZeroDivisors M₀') ≤ nonZeroDivisors M₀

Alias of comap_nonZeroDivisors_le_of_injective.

theorem mul_left_mem_nonZeroDivisors_eq_zero_iff {M₀ : Type u_1} [CommMonoidWithZero M₀] {r x : M₀} (hr : r ∈ nonZeroDivisors M₀) : r * x = 0 ↔ x = 0

@[simp]

theorem mul_left_coe_nonZeroDivisors_eq_zero_iff {M₀ : Type u_1} [CommMonoidWithZero M₀] {x : M₀} {c : ↥(nonZeroDivisors M₀)} : ↑c * x = 0 ↔ x = 0

theorem mul_mem_nonZeroDivisors {M₀ : Type u_1} [CommMonoidWithZero M₀] {a b : M₀} : a * b ∈ nonZeroDivisors M₀ ↔ a ∈ nonZeroDivisors M₀ ∧ b ∈ nonZeroDivisors M₀

theorem nonZeroDivisors_dvd_iff_dvd_coe {M₀ : Type u_1} [CommMonoidWithZero M₀] {a b : ↥(nonZeroDivisors M₀)} : a ∣ b ↔ ↑a ∣ ↑b

noncomputable def nonZeroDivisorsEquivUnits {G₀ : Type u_1} [GroupWithZero G₀] : ↥(nonZeroDivisors G₀) ≃* G₀ˣ

Canonical isomorphism between the non-zero-divisors and units of a group with zero.

Equations

• nonZeroDivisorsEquivUnits = { toFun := fun (u : ↥(nonZeroDivisors G₀)) => Units.mk0 ↑u ⋯, invFun := fun (u : G₀ˣ) => ⟨↑u, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem nonZeroDivisorsEquivUnits_symm_apply_coe {G₀ : Type u_1} [GroupWithZero G₀] (u : G₀ˣ) : ↑(nonZeroDivisorsEquivUnits.symm u) = ↑u

@[simp]

theorem nonZeroDivisorsEquivUnits_apply {G₀ : Type u_1} [GroupWithZero G₀] (u : ↥(nonZeroDivisors G₀)) : nonZeroDivisorsEquivUnits u = Units.mk0 ↑u ⋯

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

theorem mem_nonZeroSMulDivisors_iff {M₀ : Type u_1} {M : Type u_2} [MonoidWithZero M₀] [Zero M] [MulAction M₀ M] {x : M₀} : x ∈ nonZeroSMulDivisors M₀ M ↔ ∀ (m : M), x • m = 0 → m = 0

@[simp]

theorem unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors (M₀ : Type u_1) [MonoidWithZero M₀] : (nonZeroSMulDivisors M₀ᵐᵒᵖ M₀).unop = nonZeroDivisors M₀

theorem nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors (M₀ : Type u_1) [MonoidWithZero M₀] : nonZeroSMulDivisors M₀ᵐᵒᵖ M₀ = (nonZeroDivisors M₀).op

The non-zero •-divisors with • as right multiplication correspond with the non-zero divisors. Note that the MulOpposite is needed because we defined nonZeroDivisors with multiplication on the right.

def unitsNonZeroDivisorsEquiv {M₀ : Type u_1} [MonoidWithZero M₀] : (↥(nonZeroDivisors M₀))ˣ ≃* M₀ˣ

The units of the monoid of non-zero divisors of M₀ are equivalent to the units of M₀.

Equations

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

@[simp]

theorem val_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u) = ↑u

@[simp]

theorem val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = ↑u⁻¹

@[simp]

theorem unitsNonZeroDivisorsEquiv_apply {M₀ : Type u_1} [MonoidWithZero M₀] (a✝ : (↥(nonZeroDivisors M₀))ˣ) : unitsNonZeroDivisorsEquiv a✝ = (↑(Units.map (nonZeroDivisors M₀).subtype)).toFun a✝

@[simp]

theorem nonZeroDivisors.associated_coe {M₀ : Type u_1} [MonoidWithZero M₀] {a b : ↥(nonZeroDivisors M₀)} : Associated ↑a ↑b ↔ Associated a b

theorem mk_mem_nonZeroDivisors_associates {M₀ : Type u_1} [CommMonoidWithZero M₀] {a : M₀} : Associates.mk a ∈ nonZeroDivisors (Associates M₀) ↔ a ∈ nonZeroDivisors M₀

def associatesNonZeroDivisorsEquiv {M₀ : Type u_1} [CommMonoidWithZero M₀] : ↥(nonZeroDivisors (Associates M₀)) ≃* Associates ↥(nonZeroDivisors M₀)

The non-zero divisors of associates of a monoid with zero M₀ are isomorphic to the associates of the non-zero divisors of M₀ under the map ⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧.

Equations

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

@[simp]

theorem associatesNonZeroDivisorsEquiv_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : ⟦a⟧ ∈ nonZeroDivisors (Associates M₀)) : associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, ⋯⟩⟧

@[simp]

theorem associatesNonZeroDivisorsEquiv_symm_mk_mk {M₀ : Type u_1} [CommMonoidWithZero M₀] (a : M₀) (ha : a ∈ nonZeroDivisors M₀) : associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, ⋯⟩