doc-next-gen

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Module docstring

{"# 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.

"}

nonZeroDivisorsLeft definition
: Submonoid M₀
Full source 
/-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
`Submonoid`. -/
def nonZeroDivisorsLeft : Submonoid M₀ where
  carrier := {x | ∀ y, y * x = 0 → y = 0}
  one_mem' := by simp
  mul_mem' {x} {y} hx hy := fun z hz ↦ hx _ <| hy _ (mul_assoc z x y ▸ hz)
Submonoid of non-left-zero-divisors
Informal description
The submonoid of elements in a monoid with zero \( M_0 \) that are not left zero divisors, consisting of all elements \( x \in M_0 \) such that for any \( y \in M_0 \), if \( y \cdot x = 0 \) then \( y = 0 \). This submonoid contains the multiplicative identity and is closed under multiplication.
mem_nonZeroDivisorsLeft_iff theorem
: x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0
Full source 
@[simp]
lemma mem_nonZeroDivisorsLeft_iff : x ∈ nonZeroDivisorsLeft M₀x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0 := .rfl
Characterization of Non-Left-Zero-Divisors in a Monoid with Zero
Informal description
An element $x$ belongs to the submonoid of non-left-zero-divisors of $M_0$ if and only if for every element $y$ in $M_0$, the equation $y \cdot x = 0$ implies $y = 0$.
nmem_nonZeroDivisorsLeft_iff theorem
: x ∉ nonZeroDivisorsLeft M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty
Full source 
lemma nmem_nonZeroDivisorsLeft_iff :
    x ∉ nonZeroDivisorsLeft M₀x ∉ nonZeroDivisorsLeft M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty := by
  simpa [mem_nonZeroDivisorsLeft_iff] using Set.nonempty_def.symm
Characterization of Non-Membership in Non-Left-Zero-Divisors Submonoid
Informal description
An element $x$ is not in the submonoid of non-left-zero-divisors of $M_0$ if and only if there exists a nonzero element $y$ such that $y \cdot x = 0$. In other words, $x \notin M_0^{\text{left}}$ if and only if the set $\{y \mid y \cdot x = 0 \text{ and } y \neq 0\}$ is nonempty.
nonZeroDivisorsRight definition
: Submonoid M₀
Full source 
/-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
`Submonoid`. -/
def nonZeroDivisorsRight : Submonoid M₀ where
  carrier := {x | ∀ y, x * y = 0 → y = 0}
  one_mem' := by simp
  mul_mem' := fun {x} {y} hx hy z hz ↦ hy _ (hx _ ((mul_assoc x y z).symm ▸ hz))
Submonoid of non-right-zero-divisors
Informal description
The submonoid of elements in a monoid with zero that are not right zero divisors, i.e., elements \( x \) such that for all \( y \), if \( x \cdot y = 0 \) then \( y = 0 \).
mem_nonZeroDivisorsRight_iff theorem
: x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0
Full source 
@[simp]
lemma mem_nonZeroDivisorsRight_iff : x ∈ nonZeroDivisorsRight M₀x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0 := .rfl
Characterization of Non-Right-Zero-Divisors in $M₀$
Informal description
An element $x$ belongs to the submonoid of non-right-zero-divisors of $M₀$ if and only if for every element $y$ in $M₀$, the product $x \cdot y = 0$ implies $y = 0$.
nmem_nonZeroDivisorsRight_iff theorem
: x ∉ nonZeroDivisorsRight M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty
Full source 
lemma nmem_nonZeroDivisorsRight_iff :
    x ∉ nonZeroDivisorsRight M₀x ∉ nonZeroDivisorsRight M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty := by
  simpa [mem_nonZeroDivisorsRight_iff] using Set.nonempty_def.symm
Characterization of Non-Membership in Non-Right-Zero-Divisors Submonoid
Informal description
An element $x$ is not in the submonoid of non-right-zero-divisors of $M₀$ if and only if there exists a nonzero element $y$ such that $x \cdot y = 0$.
nonZeroDivisorsLeft_eq_right theorem
(M₀ : Type*) [CommMonoidWithZero M₀] : nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀
Full source 
lemma nonZeroDivisorsLeft_eq_right (M₀ : Type*) [CommMonoidWithZero M₀] :
    nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by
  ext x; simp [mul_comm x]
Equality of Left and Right Non-Zero-Divisor Submonoids in a Commutative Monoid with Zero
Informal description
For any commutative monoid with zero $M_0$, the submonoid of non-left-zero-divisors is equal to the submonoid of non-right-zero-divisors, i.e., $\text{nonZeroDivisorsLeft}(M_0) = \text{nonZeroDivisorsRight}(M_0)$.
coe_nonZeroDivisorsLeft_eq theorem
[NoZeroDivisors M₀] [Nontrivial M₀] : nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0}
Full source 
@[simp] lemma coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
    nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0} := by
  ext x
  simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and,
    Set.mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩
  contrapose! h
  exact ⟨1, h, one_ne_zero⟩
Non-left-zero-divisors coincide with nonzero elements in a nontrivial monoid with no zero divisors
Informal description
For a nontrivial monoid with zero $M_0$ that has no zero divisors, the submonoid of non-left-zero-divisors is equal to the set of all nonzero elements of $M_0$, i.e., $\text{nonZeroDivisorsLeft}(M_0) = \{x \in M_0 \mid x \neq 0\}$.
coe_nonZeroDivisorsRight_eq theorem
[NoZeroDivisors M₀] [Nontrivial M₀] : nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0}
Full source 
@[simp] lemma coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
    nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0} := by
  ext x
  simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by aesop⟩
  contrapose! h
  exact ⟨1, Or.inl h, one_ne_zero⟩
Non-right-zero-divisors coincide with nonzero elements in a nontrivial monoid with no zero divisors
Informal description
For a nontrivial monoid with zero $M_0$ that has no zero divisors, the submonoid of non-right-zero-divisors is equal to the set of all nonzero elements in $M_0$, i.e., $\text{nonZeroDivisorsRight}(M_0) = \{x \in M_0 \mid x \neq 0\}$.
nonZeroDivisors definition
(M₀ : Type*) [MonoidWithZero M₀] : Submonoid M₀
Full source 
/-- The submonoid of non-zero-divisors of a `MonoidWithZero` `M₀`. -/
def nonZeroDivisors (M₀ : Type*) [MonoidWithZero M₀] : Submonoid M₀ where
  carrier := { x | ∀ z, z * x = 0 → z = 0 }
  one_mem' _ hz := by rwa [mul_one] at hz
  mul_mem' hx₁ hx₂ _ hz := by
    rw [← mul_assoc] at hz
    exact hx₁ _ (hx₂ _ hz)
Submonoid of non-zero-divisors
Informal description
The submonoid of non-zero-divisors of a monoid with zero $M_0$ consists of all elements $x \in M_0$ such that for any $z \in M_0$, if $z \cdot x = 0$ then $z = 0$. In other words, $x$ is a non-zero-divisor if it is not a left zero divisor.
nonZeroSMulDivisors definition
(M₀ : Type*) [MonoidWithZero M₀] (M : Type*) [Zero M] [MulAction M₀ M] : Submonoid M₀
Full source 
/-- 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. -/
def nonZeroSMulDivisors (M₀ : Type*) [MonoidWithZero M₀] (M : Type*) [Zero M] [MulAction M₀ M] :
    Submonoid M₀ where
  carrier := { r | ∀ m : M, r • m = 0 → m = 0}
  one_mem' m h := (one_smul M₀ m) ▸ h
  mul_mem' {r₁ r₂} h₁ h₂ m H := h₂ _ <| h₁ _ <| mul_smul r₁ r₂ m ▸ H
Submonoid of non-zero smul-divisors (\( M \)-regular elements)
Informal description
Given a monoid with zero \( M₀ \) and an additive monoid \( M \) with a zero element and a multiplicative action of \( M₀ \) on \( M \), the submonoid of non-zero smul-divisors (also called \( M \)-regular elements) consists of all elements \( r \in M₀ \) such that for any \( m \in M \), if \( r \cdot m = 0 \) then \( m = 0 \). This submonoid is denoted by \( M₀^{⁰[M]} \).
nonZeroSMulDivisors.term_⁰[_] definition
: Lean.TrailingParserDescr✝
Full source 
/-- The notation for the submonoid of non-zero smul-divisors. -/
scoped[nonZeroSMulDivisors] notation:9000 M₀ "⁰[" M "]" => nonZeroSMulDivisors M₀ M
Notation for non-zero smul-divisors submonoid
Informal description
The notation \( M₀^{⁰[M]} \) denotes the submonoid of non-zero smul-divisors of \( M₀ \) with respect to \( M \), where \( M₀ \) is a monoid with zero and \( M \) is a type with zero equipped with a multiplicative action of \( M₀ \).
nonZeroDivisorsLeft_eq_nonZeroDivisors theorem
: nonZeroDivisorsLeft M₀ = nonZeroDivisors M₀
Full source 
lemma nonZeroDivisorsLeft_eq_nonZeroDivisors : nonZeroDivisorsLeft M₀ = nonZeroDivisors M₀ := rfl
Equality of Non-Left-Zero-Divisors and Non-Zero-Divisors Submonoids
Informal description
For a monoid with zero $M_0$, the submonoid of non-left-zero-divisors is equal to the submonoid of non-zero-divisors, i.e., $\text{nonZeroDivisorsLeft}(M_0) = \text{nonZeroDivisors}(M_0)$.
nonZeroDivisorsRight_eq_nonZeroSMulDivisors theorem
: nonZeroDivisorsRight M₀ = nonZeroSMulDivisors M₀ M₀
Full source 
lemma nonZeroDivisorsRight_eq_nonZeroSMulDivisors :
    nonZeroDivisorsRight M₀ = nonZeroSMulDivisors M₀ M₀ := rfl
Equality of Non-Right-Zero-Divisors and Self-Regular Elements Submonoids
Informal description
For a monoid with zero $M_0$, the submonoid of non-right-zero-divisors is equal to the submonoid of non-zero smul-divisors with respect to $M_0$ itself, i.e., $\text{nonZeroDivisorsRight}(M_0) = \text{nonZeroSMulDivisors}(M_0, M_0)$.
mem_nonZeroDivisors_iff theorem
: r ∈ M₀⁰ ↔ ∀ x, x * r = 0 → x = 0
Full source 
theorem mem_nonZeroDivisors_iff : r ∈ M₀⁰r ∈ M₀⁰ ↔ ∀ x, x * r = 0 → x = 0 := Iff.rfl
Characterization of Non-Zero-Divisors: $r \in M_0^0 \leftrightarrow \forall x, x \cdot r = 0 \to x = 0$
Informal description
An element $r$ belongs to the submonoid of non-zero-divisors $M_0^0$ if and only if for every element $x \in M_0$, the equation $x \cdot r = 0$ implies $x = 0$.
nmem_nonZeroDivisors_iff theorem
: r ∉ M₀⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
Full source 
lemma nmem_nonZeroDivisors_iff : r ∉ M₀⁰r ∉ M₀⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty := by
  simpa [mem_nonZeroDivisors_iff] using Set.nonempty_def.symm
Characterization of Non-Membership in Non-Zero-Divisors Submonoid
Informal description
An element $r$ does not belong to the submonoid of non-zero-divisors $M_0^0$ if and only if there exists a nonzero element $s$ such that $s \cdot r = 0$.
mul_right_mem_nonZeroDivisors_eq_zero_iff theorem
(hr : r ∈ M₀⁰) : x * r = 0 ↔ x = 0
Full source 
theorem mul_right_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : x * r = 0 ↔ x = 0 :=
  ⟨hr _, by simp +contextual⟩
Product with Non-zero-divisor Equals Zero iff Factor is Zero
Informal description
Let $M_0$ be a monoid with zero and let $r$ be a non-zero-divisor in $M_0$ (i.e., $r \in M_0^0$). Then for any element $x \in M_0$, the product $x \cdot r$ equals zero if and only if $x$ equals zero.
mul_right_coe_nonZeroDivisors_eq_zero_iff theorem
{c : M₀⁰} : x * c = 0 ↔ x = 0
Full source 
@[simp]
theorem mul_right_coe_nonZeroDivisors_eq_zero_iff {c : M₀⁰} : x * c = 0 ↔ x = 0 :=
  mul_right_mem_nonZeroDivisors_eq_zero_iff c.prop
Product with Non-zero-divisor Equals Zero iff Factor is Zero (Coe Version)
Informal description
For any element $c$ in the submonoid of non-zero-divisors $M_0^0$ of a monoid with zero $M_0$, and for any element $x \in M_0$, the product $x \cdot c$ equals zero if and only if $x$ equals zero.
IsUnit.mem_nonZeroDivisors theorem
(hx : IsUnit x) : x ∈ M₀⁰
Full source 
lemma IsUnit.mem_nonZeroDivisors (hx : IsUnit x) : x ∈ M₀⁰ := fun _ ↦ hx.mul_left_eq_zero.mp
Units are Non-Zero-Divisors
Informal description
If an element $x$ of a monoid with zero $M_0$ is a unit (i.e., invertible), then $x$ belongs to the submonoid of non-zero-divisors $M_0^0$.
zero_not_mem_nonZeroDivisors theorem
: 0 ∉ M₀⁰
Full source 
theorem zero_not_mem_nonZeroDivisors : 0 ∉ M₀⁰ := fun h ↦ one_ne_zero <| h 1 <| mul_zero _
Zero is not a non-zero-divisor
Informal description
The zero element $0$ does not belong to the submonoid of non-zero-divisors $M_0^0$ of a monoid with zero $M_0$.
nonZeroDivisors.coe_ne_zero theorem
(x : M₀⁰) : (x : M₀) ≠ 0
Full source 
@[simp]
theorem nonZeroDivisors.coe_ne_zero (x : M₀⁰) : (x : M₀) ≠ 0 := nonZeroDivisors.ne_zero x.2
Non-zero-divisors are non-zero (coercion form)
Informal description
For any element $x$ in the submonoid of non-zero-divisors $M_0^0$ of a monoid with zero $M_0$, the underlying element $(x : M_0)$ is not equal to zero.
instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero instance
[IsLeftCancelMulZero M₀] : LeftCancelMonoid M₀⁰
Full source 
instance [IsLeftCancelMulZero M₀] :
    LeftCancelMonoid M₀⁰ where
  mul_left_cancel _ _ _ h :=  Subtype.ext <|
    mul_left_cancel₀ (nonZeroDivisors.coe_ne_zero _) (by
      simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h)
Left-Cancellative Monoid Structure on Non-Zero-Divisors
Informal description
For any monoid with zero $M_0$ that satisfies the left cancellation property for multiplication (i.e., $a \cdot b = a \cdot c$ implies $b = c$ for any $a, b, c \in M_0$), the submonoid of non-zero-divisors $M_0^0$ inherits a left-cancellative monoid structure.
instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero instance
[IsRightCancelMulZero M₀] : RightCancelMonoid M₀⁰
Full source 
instance [IsRightCancelMulZero M₀] :
    RightCancelMonoid M₀⁰ where
  mul_right_cancel _ _ _ h := Subtype.ext <|
    mul_right_cancel₀ (nonZeroDivisors.coe_ne_zero _) (by
      simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h)
Right-Cancellative Monoid Structure on Non-Zero-Divisors
Informal description
For any monoid with zero $M_0$ that satisfies the right cancellation property with respect to zero (i.e., for any $x, y, z \in M_0$, if $x \cdot z = y \cdot z$ and $z \neq 0$, then $x = y$), the submonoid of non-zero-divisors $M_0^0$ inherits a right-cancellative monoid structure from $M_0$.
mem_nonZeroDivisors_of_ne_zero theorem
(hx : x ≠ 0) : x ∈ M₀⁰
Full source 
theorem mem_nonZeroDivisors_of_ne_zero (hx : x ≠ 0) : x ∈ M₀⁰ := fun _ ↦
  eq_zero_of_ne_zero_of_mul_right_eq_zero hx
Nonzero Elements are Non-zero-divisors
Informal description
For any element $x$ in a monoid with zero $M_0$, if $x$ is nonzero ($x \neq 0$), then $x$ belongs to the submonoid of non-zero-divisors $M_0^0$.
mem_nonZeroDivisors_iff_ne_zero theorem
[Nontrivial M₀] : x ∈ M₀⁰ ↔ x ≠ 0
Full source 
@[simp] lemma mem_nonZeroDivisors_iff_ne_zero [Nontrivial M₀] : x ∈ M₀⁰x ∈ M₀⁰ ↔ x ≠ 0 :=
  ⟨nonZeroDivisors.ne_zero, mem_nonZeroDivisors_of_ne_zero⟩
Characterization of Non-zero-divisors in Nontrivial Monoids: $x \in M_0^0 \leftrightarrow x \neq 0$
Informal description
In a nontrivial monoid with zero $M_0$, an element $x$ belongs to the submonoid of non-zero-divisors $M_0^0$ if and only if $x$ is not equal to zero, i.e., $x \neq 0$.
le_nonZeroDivisors_of_noZeroDivisors theorem
{S : Submonoid M₀} (hS : (0 : M₀) ∉ S) : S ≤ M₀⁰
Full source 
theorem le_nonZeroDivisors_of_noZeroDivisors {S : Submonoid M₀} (hS : (0 : M₀) ∉ S) :
    S ≤ M₀⁰ := fun _ hx _ hy ↦
  (eq_zero_or_eq_zero_of_mul_eq_zero hy).resolve_right (ne_of_mem_of_not_mem hx hS)
Submonoid Exclusion of Zero Implies Non-zero-divisors
Informal description
For any submonoid $S$ of a monoid with zero $M_0$, if $0 \notin S$, then $S$ is contained in the submonoid of non-zero-divisors $M_0^0$.
powers_le_nonZeroDivisors_of_noZeroDivisors theorem
(hx : x ≠ 0) : Submonoid.powers x ≤ M₀⁰
Full source 
theorem powers_le_nonZeroDivisors_of_noZeroDivisors (hx : x ≠ 0) : Submonoid.powers x ≤ M₀⁰ :=
  le_nonZeroDivisors_of_noZeroDivisors fun h ↦ hx (h.recOn fun _ ↦ pow_eq_zero)
Powers of Nonzero Elements are Non-zero-divisors
Informal description
For any element $x$ in a monoid with zero $M_0$, if $x$ is nonzero, then the submonoid generated by the powers of $x$ is contained in the submonoid of non-zero-divisors $M_0^0$.
map_ne_zero_of_mem_nonZeroDivisors theorem
[Nontrivial M₀] [ZeroHomClass F M₀ M₀'] (g : F) (hg : Injective (g : M₀ → M₀')) {x : M₀} (h : x ∈ M₀⁰) : g x ≠ 0
Full source 
theorem map_ne_zero_of_mem_nonZeroDivisors [Nontrivial M₀] [ZeroHomClass F M₀ M₀'] (g : F)
    (hg : Injective (g : M₀ → M₀')) {x : M₀} (h : x ∈ M₀⁰) : g x ≠ 0 := fun h0 ↦
  one_ne_zero (h 1 ((one_mul x).symm ▸ hg (h0.trans (map_zero g).symm)))
Nonzero Image of Non-Zero-Divisors under Injective Zero-Preserving Homomorphisms
Informal description
Let $M_0$ and $M_0'$ be nontrivial monoids with zero, and let $F$ be a type of zero-preserving homomorphisms from $M_0$ to $M_0'$. Given an injective homomorphism $g \in F$ and an element $x \in M_0$ that is a non-zero-divisor (i.e., $x \in M_0^0$), the image $g(x)$ is nonzero in $M_0'$.
map_mem_nonZeroDivisors theorem
[Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F) (hg : Injective g) {x : M₀} (h : x ∈ M₀⁰) : g x ∈ M₀'⁰
Full source 
theorem map_mem_nonZeroDivisors [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F)
    (hg : Injective g) {x : M₀} (h : x ∈ M₀⁰) : g x ∈ M₀'⁰ := fun _ hz ↦
  eq_zero_of_ne_zero_of_mul_right_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h) hz
Injective Zero-Preserving Homomorphisms Preserve Non-Zero-Divisors
Informal description
Let $M_0$ and $M_0'$ be nontrivial monoids with zero, where $M_0'$ has no zero divisors. Let $F$ be a type of zero-preserving homomorphisms from $M_0$ to $M_0'$. Given an injective homomorphism $g \in F$ and an element $x \in M_0$ that is a non-zero-divisor (i.e., $x \in M_0^0$), the image $g(x)$ is also a non-zero-divisor in $M_0'$ (i.e., $g(x) \in M_0'^0$).
MulEquivClass.map_nonZeroDivisors theorem
{M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S] [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) : Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S
Full source 
theorem MulEquivClass.map_nonZeroDivisors {M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S]
    [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) :
    Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S := by
  let h : M₀ ≃* S := h
  show Submonoid.map h _ = _
  ext
  simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
    ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul,
    map_eq_zero_iff _ h.symm.injective]
Multiplicative Equivalence Preserves Non-Zero-Divisors: $h(M_0^0) = S^0$
Informal description
Let $M_0$ and $S$ be monoids with zero, and let $F$ be a type of multiplicative equivalences between $M_0$ and $S$ (i.e., bijective maps preserving multiplication and zero). For any multiplicative equivalence $h \in F$, the image of the submonoid of non-zero-divisors of $M_0$ under $h$ is equal to the submonoid of non-zero-divisors of $S$. In other words, \[ h(M_0^0) = S^0, \] where $M_0^0$ and $S^0$ denote the submonoids of non-zero-divisors in $M_0$ and $S$ respectively.
map_le_nonZeroDivisors_of_injective theorem
[NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Injective f) {S : Submonoid M₀} (hS : S ≤ M₀⁰) : S.map f ≤ M₀'⁰
Full source 
theorem map_le_nonZeroDivisors_of_injective [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀']
    (f : F) (hf : Injective f) {S : Submonoid M₀} (hS : S ≤ M₀⁰) : S.map f ≤ M₀'⁰ := by
  cases subsingleton_or_nontrivial M₀
  · simp [Subsingleton.elim S ⊥]
  · refine le_nonZeroDivisors_of_noZeroDivisors ?_
    rintro ⟨x, hx, hx0⟩
    exact zero_not_mem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx
Injective Homomorphisms Preserve Non-Zero-Divisor Submonoids: $f(S) \subseteq M_0'^0$
Informal description
Let $M_0$ and $M_0'$ be monoids with zero, where $M_0'$ has no zero divisors. Given an injective homomorphism $f \colon M_0 \to M_0'$ and a submonoid $S$ of $M_0$ consisting of non-zero-divisors (i.e., $S \subseteq M_0^0$), the image of $S$ under $f$ is contained in the submonoid of non-zero-divisors of $M_0'$ (i.e., $f(S) \subseteq M_0'^0$).
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective theorem
[NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Injective f) : M₀⁰ ≤ M₀'⁰.comap f
Full source 
theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M₀']
    [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Injective f) : M₀⁰ ≤ M₀'⁰.comap f :=
  Submonoid.le_comap_of_map_le _ (map_le_nonZeroDivisors_of_injective _ hf le_rfl)
Inclusion of Non-Zero-Divisors in Preimage under Injective Homomorphism: $M_0^0 \subseteq f^{-1}(M_0'^0)$
Informal description
Let $M_0$ and $M_0'$ be monoids with zero, where $M_0'$ has no zero divisors. Given an injective homomorphism $f \colon M_0 \to M_0'$, the submonoid of non-zero-divisors of $M_0$ is contained in the preimage under $f$ of the submonoid of non-zero-divisors of $M_0'$. In other words, \[ M_0^0 \subseteq f^{-1}(M_0'^0). \]
mem_nonZeroDivisors_of_injective theorem
[MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Injective f) (hx : f x ∈ M₀'⁰) : x ∈ M₀⁰
Full source 
/-- If an element maps to a non-zero-divisor via injective homomorphism,
then it is a non-zero-divisor. -/
theorem mem_nonZeroDivisors_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F}
    (hf : Injective f) (hx : f x ∈ M₀'⁰) : x ∈ M₀⁰ :=
  fun y hy ↦ hf <| map_zero f ▸ hx (f y) (map_mul f y x ▸ map_zero f ▸ congrArg f hy)
Injective Homomorphisms Preserve Non-Zero-Divisors
Informal description
Let $M_0$ and $M_0'$ be monoids with zero, and let $f \colon M_0 \to M_0'$ be an injective homomorphism. If $f(x)$ is a non-zero-divisor in $M_0'$, then $x$ is a non-zero-divisor in $M_0$.
comap_nonZeroDivisors_le_of_injective theorem
[MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Injective f) : M₀'⁰.comap f ≤ M₀⁰
Full source 
theorem comap_nonZeroDivisors_le_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F}
    (hf : Injective f) : M₀'⁰.comap f ≤ M₀⁰ :=
  fun _ ha ↦ mem_nonZeroDivisors_of_injective hf (Submonoid.mem_comap.mp ha)
Preimage of Non-Zero-Divisors under Injective Homomorphism is Contained in Non-Zero-Divisors
Informal description
Let $M_0$ and $M_0'$ be monoids with zero, and let $f \colon M_0 \to M_0'$ be an injective homomorphism. Then the preimage of the submonoid of non-zero-divisors of $M_0'$ under $f$ is contained in the submonoid of non-zero-divisors of $M_0$. In other words, if $x \in M_0$ is such that $f(x)$ is a non-zero-divisor in $M_0'$, then $x$ is a non-zero-divisor in $M_0$.
mul_left_mem_nonZeroDivisors_eq_zero_iff theorem
(hr : r ∈ M₀⁰) : r * x = 0 ↔ x = 0
Full source 
lemma mul_left_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : r * x = 0 ↔ x = 0 := by
  rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
Left Multiplication by Non-zero-divisor Equals Zero iff Factor is Zero
Informal description
Let $M_0$ be a monoid with zero and let $r$ be a non-zero-divisor in $M_0$ (i.e., $r \in M_0^0$). Then for any element $x \in M_0$, the product $r \cdot x$ equals zero if and only if $x$ equals zero.
mul_left_coe_nonZeroDivisors_eq_zero_iff theorem
{c : M₀⁰} : (c : M₀) * x = 0 ↔ x = 0
Full source 
@[simp]
lemma mul_left_coe_nonZeroDivisors_eq_zero_iff {c : M₀⁰} : (c : M₀) * x = 0 ↔ x = 0 :=
  mul_left_mem_nonZeroDivisors_eq_zero_iff c.prop
Left Multiplication by Non-zero-divisor Coefficient Equals Zero iff Factor is Zero
Informal description
For any element $c$ in the submonoid of non-zero-divisors $M_0^0$ of a monoid with zero $M_0$, and for any element $x \in M_0$, the product $(c : M_0) \cdot x$ equals zero if and only if $x$ equals zero.
mul_mem_nonZeroDivisors theorem
: a * b ∈ M₀⁰ ↔ a ∈ M₀⁰ ∧ b ∈ M₀⁰
Full source 
lemma mul_mem_nonZeroDivisors : a * b ∈ M₀⁰a * b ∈ M₀⁰ ↔ a ∈ M₀⁰ ∧ b ∈ M₀⁰ where
  mp h := by
    constructor <;> intro x h' <;> apply h
    · rw [← mul_assoc, h', zero_mul]
    · rw [mul_comm a b, ← mul_assoc, h', zero_mul]
  mpr := by
    rintro ⟨ha, hb⟩ x hx
    apply ha
    apply hb
    rw [mul_assoc, hx]
Product of Non-zero-divisors is a Non-zero-divisor if and only if Both Factors Are
Informal description
For any elements $a$ and $b$ in a monoid with zero $M_0$, the product $a * b$ belongs to the submonoid of non-zero-divisors $M_0^0$ if and only if both $a$ and $b$ belong to $M_0^0$.
nonZeroDivisorsEquivUnits definition
: G₀⁰ ≃* G₀ˣ
Full source 
/-- Canonical isomorphism between the non-zero-divisors and units of a group with zero. -/
@[simps]
noncomputable def nonZeroDivisorsEquivUnits : G₀⁰G₀⁰ ≃* G₀ˣ where
  toFun u := .mk0 _ <| mem_nonZeroDivisors_iff_ne_zero.1 u.2
  invFun u := ⟨u, u.isUnit.mem_nonZeroDivisors⟩
  left_inv u := rfl
  right_inv u := by simp
  map_mul' u v := by simp
Isomorphism between non-zero-divisors and units in a group with zero
Informal description
The canonical multiplicative isomorphism between the submonoid of non-zero-divisors $G_0^0$ and the group of units $G_0^\times$ of a group with zero $G_0$. Specifically, it maps each non-zero-divisor $x \in G_0^0$ to the unit $\text{mk0}(x)$, where $\text{mk0}$ constructs a unit from $x$ using the property that $x$ is not a zero divisor. The inverse map sends each unit $u \in G_0^\times$ back to the non-zero-divisor $\langle u, u.\text{isUnit}.\text{mem\_nonZeroDivisors} \rangle$.
mem_nonZeroSMulDivisors_iff theorem
: x ∈ M₀⁰[M] ↔ ∀ (m : M), x • m = 0 → m = 0
Full source 
lemma mem_nonZeroSMulDivisors_iff : x ∈ M₀⁰[M]x ∈ M₀⁰[M] ↔ ∀ (m : M), x • m = 0 → m = 0 := Iff.rfl
Characterization of Non-Zero Smul-Divisors: $x \in M_0^{⁰[M]} \leftrightarrow \forall m \in M, x \cdot m = 0 \rightarrow m = 0$
Informal description
An element $x$ of a monoid with zero $M_0$ belongs to the submonoid of non-zero smul-divisors $M_0^{⁰[M]}$ (with respect to a monoid $M$ with zero and a multiplicative action of $M_0$ on $M$) if and only if for every $m \in M$, the condition $x \cdot m = 0$ implies $m = 0$.
unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors theorem
: (M₀ᵐᵒᵖ⁰[M₀]).unop = M₀⁰
Full source 
@[simp]
lemma unop_nonZeroSMulDivisors_mulOpposite_eq_nonZeroDivisors :
    (M₀ᵐᵒᵖM₀ᵐᵒᵖ ⁰[M₀]).unop = M₀⁰ := rfl
Equality of Unopposed Non-Zero Smul-Divisors and Non-Zero-Divisors: $\text{unop}(M_0^\text{op}{}^{⁰[M_0]}) = M_0^0$
Informal description
Let $M_0$ be a monoid with zero. The submonoid of non-zero smul-divisors of the multiplicative opposite $M_0^\text{op}$ acting on $M_0$, when mapped back to $M_0$ via the `unop` operation, equals the submonoid of non-zero-divisors of $M_0$. In symbols: $$ \text{unop}(M_0^\text{op}{}^{⁰[M_0]}) = M_0^0. $$
nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors theorem
: M₀ᵐᵒᵖ⁰[M₀] = M₀⁰.op
Full source 
/-- 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. -/
lemma nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors :
    M₀ᵐᵒᵖM₀ᵐᵒᵖ ⁰[M₀] = M₀⁰.op := rfl
Equality of Non-Zero Smul-Divisors and Opposite Non-Zero-Divisors: $M_0^\text{op}^{⁰[M_0]} = M_0^0^\text{op}$
Informal description
The submonoid of non-zero smul-divisors of the multiplicative opposite monoid $M_0^\text{op}$ with respect to $M_0$ is equal to the opposite submonoid of the non-zero-divisors of $M_0$. In other words, $M_0^\text{op}^{⁰[M_0]} = M_0^0^\text{op}$.
unitsNonZeroDivisorsEquiv definition
: M₀⁰ˣ ≃* M₀ˣ
Full source 
/-- The units of the monoid of non-zero divisors of `M₀` are equivalent to the units of `M₀`. -/
@[simps]
def unitsNonZeroDivisorsEquiv : M₀⁰M₀⁰ˣM₀⁰ˣ ≃* M₀ˣ where
  __ := Units.map M₀⁰.subtype
  invFun u := ⟨⟨u, u.isUnit.mem_nonZeroDivisors⟩, ⟨(u⁻¹ : M₀ˣ), u⁻¹.isUnit.mem_nonZeroDivisors⟩,
    by simp, by simp⟩
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between units of non-zero-divisors and units of the monoid
Informal description
The multiplicative equivalence between the group of units of the submonoid of non-zero-divisors of a monoid with zero $M_0$ and the group of units of $M_0$ itself. Specifically, it states that the units of $M_0^0$ (the submonoid of non-zero-divisors) are isomorphic to the units of $M_0$ as multiplicative groups.
nonZeroDivisors.associated_coe theorem
: Associated (a : M₀) b ↔ Associated a b
Full source 
@[simp, norm_cast] lemma nonZeroDivisors.associated_coe : AssociatedAssociated (a : M₀) b ↔ Associated a b :=
  unitsNonZeroDivisorsEquiv.symm.exists_congr_left.trans <| by simp [Associated]; norm_cast
Preservation of Associatedness in Non-Zero-Divisors Submonoid: $\text{Associated}(a,b) \leftrightarrow \text{Associated}(a,b)$
Informal description
For any elements $a$ and $b$ in a monoid with zero $M_0$, the element $a$ considered as a member of the submonoid of non-zero-divisors is associated to $b$ if and only if $a$ is associated to $b$ in $M_0$ itself. In other words, the associatedness relation is preserved when viewing $a$ as an element of the non-zero-divisors submonoid.
mk_mem_nonZeroDivisors_associates theorem
: Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰
Full source 
theorem mk_mem_nonZeroDivisors_associates : Associates.mkAssociates.mk a ∈ (Associates M₀)⁰Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰ := by
  rw [mem_nonZeroDivisors_iff, mem_nonZeroDivisors_iff, ← not_iff_not]
  push_neg
  constructor
  · rintro ⟨⟨x⟩, hx₁, hx₂⟩
    refine ⟨x, ?_, ?_⟩
    · rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
    · rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]
  · refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
    rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]
Membership in Non-Zero-Divisors of Associates Monoid: $\text{Associates.mk}(a) \in (\text{Associates}(M_0))^0 \leftrightarrow a \in M_0^0$
Informal description
For any element $a$ in a monoid with zero $M_0$, the equivalence class $\text{Associates.mk}(a)$ belongs to the submonoid of non-zero-divisors of the monoid of associates $\text{Associates}(M_0)$ if and only if $a$ itself belongs to the submonoid of non-zero-divisors of $M_0$. In other words, $\text{Associates.mk}(a) \in (\text{Associates}(M_0))^0 \leftrightarrow a \in M_0^0$.
associatesNonZeroDivisorsEquiv definition
: (Associates M₀)⁰ ≃* Associates M₀⁰
Full source 
/-- 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, _⟩⟧`. -/
def associatesNonZeroDivisorsEquiv : (Associates M₀)⁰(Associates M₀)⁰ ≃* Associates M₀⁰ where
  toEquiv := .subtypeQuotientEquivQuotientSubtype _ (s₂ := Associated.setoid _)
    (· ∈ nonZeroDivisors _)
    (by simp [mem_nonZeroDivisors_iff, Quotient.forall, Associates.mk_mul_mk])
    (by simp [Associated.setoid])
  map_mul' := by simp [Quotient.forall, Associates.mk_mul_mk]
Isomorphism between non-zero divisors of associates and associates of non-zero divisors
Informal description
The non-zero divisors of the monoid of associates of a monoid with zero $M_0$ are multiplicatively isomorphic to the monoid of associates of the non-zero divisors of $M_0$. Specifically, the isomorphism maps the equivalence class $\llbracket a \rrbracket$ of a non-zero-divisor $a \in M_0$ to the equivalence class $\llbracket \langle a, h \rangle \rrbracket$, where $h$ is the proof that $a$ is a non-zero-divisor.
associatesNonZeroDivisorsEquiv_mk_mk theorem
(a : M₀) (ha) : associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, mk_mem_nonZeroDivisors_associates.1 ha⟩⟧
Full source 
@[simp]
lemma associatesNonZeroDivisorsEquiv_mk_mk (a : M₀) (ha) :
    associatesNonZeroDivisorsEquiv ⟨⟦a⟧, ha⟩ = ⟦⟨a, mk_mem_nonZeroDivisors_associates.1 ha⟩⟧ := rfl
Action of Non-Zero-Divisor Isomorphism on Equivalence Classes
Informal description
For any element $a$ in a monoid with zero $M_0$ and any proof $ha$ that the equivalence class $\llbracket a \rrbracket$ belongs to the submonoid of non-zero-divisors of the monoid of associates $\text{Associates}(M_0)$, the multiplicative isomorphism $\text{associatesNonZeroDivisorsEquiv}$ maps the pair $\langle \llbracket a \rrbracket, ha \rangle$ to the equivalence class $\llbracket \langle a, h \rangle \rrbracket$, where $h$ is the proof that $a$ itself is a non-zero-divisor in $M_0$ (obtained from $ha$ via $\text{mk\_mem\_nonZeroDivisors\_associates.1}$).
associatesNonZeroDivisorsEquiv_symm_mk_mk theorem
(a : M₀) (ha) : associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, mk_mem_nonZeroDivisors_associates.2 ha⟩
Full source 
@[simp]
lemma associatesNonZeroDivisorsEquiv_symm_mk_mk (a : M₀) (ha) :
    associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, mk_mem_nonZeroDivisors_associates.2 ha⟩ :=
  rfl
Inverse of Associates Non-Zero-Divisors Isomorphism Applied to Equivalence Class
Informal description
For any element $a$ in a monoid with zero $M_0$ and any proof $ha$ that $a$ is a non-zero-divisor, the inverse of the multiplicative isomorphism `associatesNonZeroDivisorsEquiv` maps the equivalence class $\llbracket \langle a, ha \rangle \rrbracket$ in the monoid of associates of non-zero-divisors of $M_0$ to the pair $\langle \llbracket a \rrbracket, h \rangle$, where $h$ is the proof that $\llbracket a \rrbracket$ is a non-zero-divisor in the monoid of associates of $M_0$.