doc-next-gen

Mathlib.Algebra.GroupWithZero.Associated

Module docstring

{"# Associated elements.

In this file we define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient. "}

Associated definition
[Monoid M] (x y : M) : Prop
Full source 
/-- Two elements of a `Monoid` are `Associated` if one of them is another one
multiplied by a unit on the right. -/
def Associated [Monoid M] (x y : M) : Prop :=
  ∃ u : Mˣ, x * u = y
Associated elements in a monoid
Informal description
Two elements $x$ and $y$ of a monoid $M$ are called *associated* (denoted $x \sim y$) if there exists a unit $u$ in $M$ such that $x \cdot u = y$. In other words, $y$ can be obtained from $x$ by right-multiplication with an invertible element.
Associated.refl theorem
[Monoid M] (x : M) : x ~ᵤ x
Full source 
@[refl]
protected theorem refl [Monoid M] (x : M) : x ~ᵤ x :=
  ⟨1, by simp⟩
Reflexivity of the Associated Relation in a Monoid
Informal description
For any element $x$ in a monoid $M$, $x$ is associated with itself, i.e., $x \sim x$.
Associated.rfl theorem
[Monoid M] {x : M} : x ~ᵤ x
Full source 
protected theorem rfl [Monoid M] {x : M} : x ~ᵤ x :=
  .refl x
Reflexivity of the Associated Relation
Informal description
For any element $x$ in a monoid $M$, $x$ is associated with itself, i.e., $x \sim x$.
Associated.instIsRefl instance
[Monoid M] : IsRefl M Associated
Full source 
instance [Monoid M] : IsRefl M Associated :=
  ⟨Associated.refl⟩
Reflexivity of the Associated Relation in a Monoid
Informal description
For any monoid $M$, the relation of being associated elements (denoted by $\sim$) is reflexive. That is, every element $x \in M$ satisfies $x \sim x$.
Associated.symm theorem
[Monoid M] : ∀ {x y : M}, x ~ᵤ y → y ~ᵤ x
Full source 
@[symm]
protected theorem symm [Monoid M] : ∀ {x y : M}, x ~ᵤ y → y ~ᵤ x
  | x, _, ⟨u, rfl⟩ => ⟨u⁻¹, by rw [mul_assoc, Units.mul_inv, mul_one]⟩
Symmetry of the Associated Relation in a Monoid
Informal description
For any elements $x$ and $y$ in a monoid $M$, if $x$ is associated to $y$ (i.e., there exists a unit $u$ such that $x \cdot u = y$), then $y$ is associated to $x$ (i.e., there exists a unit $v$ such that $y \cdot v = x$).
Associated.instIsSymm instance
[Monoid M] : IsSymm M Associated
Full source 
instance [Monoid M] : IsSymm M Associated :=
  ⟨fun _ _ => Associated.symm⟩
Symmetry of the Associated Elements Relation
Informal description
For any monoid $M$, the relation $\sim$ of being associated elements is symmetric. That is, for any $x, y \in M$, if $x \sim y$ then $y \sim x$.
Associated.comm theorem
[Monoid M] {x y : M} : x ~ᵤ y ↔ y ~ᵤ x
Full source 
protected theorem comm [Monoid M] {x y : M} : x ~ᵤ yx ~ᵤ y ↔ y ~ᵤ x :=
  ⟨Associated.symm, Associated.symm⟩
Symmetry of the Associated Relation: $x \sim y \leftrightarrow y \sim x$
Informal description
For any elements $x$ and $y$ in a monoid $M$, $x$ is associated to $y$ if and only if $y$ is associated to $x$. In other words, the associated relation is symmetric: $x \sim y \leftrightarrow y \sim x$.
Associated.trans theorem
[Monoid M] : ∀ {x y z : M}, x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
Full source 
@[trans]
protected theorem trans [Monoid M] : ∀ {x y z : M}, x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
  | x, _, _, ⟨u, rfl⟩, ⟨v, rfl⟩ => ⟨u * v, by rw [Units.val_mul, mul_assoc]⟩
Transitivity of the Associated Relation in a Monoid
Informal description
For any elements $x, y, z$ in a monoid $M$, if $x$ is associated to $y$ and $y$ is associated to $z$, then $x$ is associated to $z$. In other words, the associated relation is transitive.
Associated.instIsTrans instance
[Monoid M] : IsTrans M Associated
Full source 
instance [Monoid M] : IsTrans M Associated :=
  ⟨fun _ _ _ => Associated.trans⟩
Transitivity of the Associated Relation in a Monoid
Informal description
For any monoid $M$, the relation of being associated elements (denoted by $\sim$) is transitive. That is, for any elements $x, y, z \in M$, if $x \sim y$ and $y \sim z$, then $x \sim z$.
Associated.setoid definition
(M : Type*) [Monoid M] : Setoid M
Full source 
/-- The setoid of the relation `x ~ᵤ y` iff there is a unit `u` such that `x * u = y` -/
protected def setoid (M : Type*) [Monoid M] :
    Setoid M where
  r := Associated
  iseqv := ⟨Associated.refl, Associated.symm, Associated.trans⟩
Setoid of associated elements in a monoid
Informal description
The setoid (equivalence relation) on a monoid $M$ where two elements $x$ and $y$ are related if and only if they are *associated*, i.e., there exists a unit $u$ in $M$ such that $x \cdot u = y$. This relation is reflexive, symmetric, and transitive.
Associated.map theorem
{M N : Type*} [Monoid M] [Monoid N] {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x y : M} (ha : Associated x y) : Associated (f x) (f y)
Full source 
theorem map {M N : Type*} [Monoid M] [Monoid N] {F : Type*} [FunLike F M N] [MonoidHomClass F M N]
    (f : F) {x y : M} (ha : Associated x y) : Associated (f x) (f y) := by
  obtain ⟨u, ha⟩ := ha
  exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩
Monoid Homomorphisms Preserve Associated Elements
Informal description
Let $M$ and $N$ be monoids, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserves the monoid structure. For any homomorphism $f \in F$ and any elements $x, y \in M$ that are associated (i.e., $x \sim y$), their images under $f$ are also associated in $N$ (i.e., $f(x) \sim f(y)$).
unit_associated_one theorem
[Monoid M] {u : Mˣ} : (u : M) ~ᵤ 1
Full source 
theorem unit_associated_one [Monoid M] {u : Mˣ} : (u : M) ~ᵤ 1 :=
  ⟨u⁻¹, Units.mul_inv u⟩
Unit Associated with Identity in a Monoid
Informal description
For any unit $u$ in the group of units $M^\times$ of a monoid $M$, the element $u$ (considered as an element of $M$) is associated with the multiplicative identity $1$, i.e., $u \sim 1$.
associated_one_iff_isUnit theorem
[Monoid M] {a : M} : (a : M) ~ᵤ 1 ↔ IsUnit a
Full source 
@[simp]
theorem associated_one_iff_isUnit [Monoid M] {a : M} : (a : M) ~ᵤ 1(a : M) ~ᵤ 1 ↔ IsUnit a :=
  Iff.intro
    (fun h =>
      let ⟨c, h⟩ := h.symm
      h ▸ ⟨c, (one_mul _).symm⟩)
    fun ⟨c, h⟩ => Associated.symm ⟨c, by simp [h]⟩
Characterization of Units via Association with Identity: $a \sim 1 \leftrightarrow \text{IsUnit}(a)$
Informal description
For any element $a$ in a monoid $M$, $a$ is associated with the multiplicative identity $1$ (i.e., $a \sim 1$) if and only if $a$ is a unit in $M$.
associated_one_of_mul_eq_one theorem
[CommMonoid M] {a : M} (b : M) (hab : a * b = 1) : a ~ᵤ 1
Full source 
theorem associated_one_of_mul_eq_one [CommMonoid M] {a : M} (b : M) (hab : a * b = 1) : a ~ᵤ 1 :=
  show (Units.mkOfMulEqOne a b hab : M) ~ᵤ 1 from unit_associated_one
Product with Identity Implies Association: $a \cdot b = 1 \Rightarrow a \sim 1$
Informal description
Let $M$ be a commutative monoid. For any elements $a, b \in M$ such that $a \cdot b = 1$, the element $a$ is associated with the multiplicative identity $1$, i.e., $a \sim 1$.
associated_one_of_associated_mul_one theorem
[CommMonoid M] {a b : M} : a * b ~ᵤ 1 → a ~ᵤ 1
Full source 
theorem associated_one_of_associated_mul_one [CommMonoid M] {a b : M} : a * b ~ᵤ 1 → a ~ᵤ 1
  | ⟨u, h⟩ => associated_one_of_mul_eq_one (b * u) <| by simpa [mul_assoc] using h
Association of Factor When Product is Associated to One
Informal description
Let $M$ be a commutative monoid. For any elements $a, b \in M$, if the product $a \cdot b$ is associated with the multiplicative identity $1$, then $a$ is also associated with $1$, i.e., $a \cdot b \sim 1$ implies $a \sim 1$.
associated_mul_unit_left theorem
{N : Type*} [Monoid N] (a u : N) (hu : IsUnit u) : Associated (a * u) a
Full source 
theorem associated_mul_unit_left {N : Type*} [Monoid N] (a u : N) (hu : IsUnit u) :
    Associated (a * u) a :=
  let ⟨u', hu⟩ := hu
  ⟨u'⁻¹, hu ▸ Units.mul_inv_cancel_right _ _⟩
Left multiplication by a unit preserves association
Informal description
Let $M$ be a monoid, and let $a, u \in M$ with $u$ being a unit. Then the element $a \cdot u$ is associated to $a$, i.e., $a \cdot u \sim a$.
associated_unit_mul_left theorem
{N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) : Associated (u * a) a
Full source 
theorem associated_unit_mul_left {N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) :
    Associated (u * a) a := by
  rw [mul_comm]
  exact associated_mul_unit_left _ _ hu
Left multiplication by a unit preserves association in a commutative monoid
Informal description
Let $M$ be a commutative monoid, and let $a, u \in M$ with $u$ being a unit. Then the element $u \cdot a$ is associated to $a$, i.e., $u \cdot a \sim a$.
associated_mul_unit_right theorem
{N : Type*} [Monoid N] (a u : N) (hu : IsUnit u) : Associated a (a * u)
Full source 
theorem associated_mul_unit_right {N : Type*} [Monoid N] (a u : N) (hu : IsUnit u) :
    Associated a (a * u) :=
  (associated_mul_unit_left a u hu).symm
Right multiplication by a unit preserves association
Informal description
Let $M$ be a monoid, and let $a, u \in M$ with $u$ being a unit. Then the element $a$ is associated to $a \cdot u$, i.e., $a \sim a \cdot u$.
associated_unit_mul_right theorem
{N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) : Associated a (u * a)
Full source 
theorem associated_unit_mul_right {N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) :
    Associated a (u * a) :=
  (associated_unit_mul_left a u hu).symm
Right multiplication by a unit preserves association in a commutative monoid
Informal description
Let $M$ be a commutative monoid, and let $a, u \in M$ with $u$ being a unit. Then the element $a$ is associated to $u \cdot a$, i.e., $a \sim u \cdot a$.
associated_mul_isUnit_left_iff theorem
{N : Type*} [Monoid N] {a u b : N} (hu : IsUnit u) : Associated (a * u) b ↔ Associated a b
Full source 
theorem associated_mul_isUnit_left_iff {N : Type*} [Monoid N] {a u b : N} (hu : IsUnit u) :
    AssociatedAssociated (a * u) b ↔ Associated a b :=
  ⟨(associated_mul_unit_right _ _ hu).trans, (associated_mul_unit_left _ _ hu).trans⟩
Left Multiplication by Unit Preserves Association Equivalence
Informal description
Let $M$ be a monoid, and let $a, u, b \in M$ with $u$ being a unit. Then the element $a \cdot u$ is associated to $b$ if and only if $a$ is associated to $b$, i.e., $a \cdot u \sim b \leftrightarrow a \sim b$.
associated_isUnit_mul_left_iff theorem
{N : Type*} [CommMonoid N] {u a b : N} (hu : IsUnit u) : Associated (u * a) b ↔ Associated a b
Full source 
theorem associated_isUnit_mul_left_iff {N : Type*} [CommMonoid N] {u a b : N} (hu : IsUnit u) :
    AssociatedAssociated (u * a) b ↔ Associated a b := by
  rw [mul_comm]
  exact associated_mul_isUnit_left_iff hu
Left Multiplication by Unit Preserves Association Equivalence in Commutative Monoid
Informal description
Let $M$ be a commutative monoid, and let $a, b, u \in M$ with $u$ being a unit. Then the element $u \cdot a$ is associated to $b$ if and only if $a$ is associated to $b$, i.e., $u \cdot a \sim b \leftrightarrow a \sim b$.
associated_mul_isUnit_right_iff theorem
{N : Type*} [Monoid N] {a b u : N} (hu : IsUnit u) : Associated a (b * u) ↔ Associated a b
Full source 
theorem associated_mul_isUnit_right_iff {N : Type*} [Monoid N] {a b u : N} (hu : IsUnit u) :
    AssociatedAssociated a (b * u) ↔ Associated a b :=
  Associated.comm.trans <| (associated_mul_isUnit_left_iff hu).trans Associated.comm
Right Multiplication by Unit Preserves Association Equivalence
Informal description
Let $M$ be a monoid, and let $a, b, u \in M$ with $u$ being a unit. Then $a$ is associated to $b \cdot u$ if and only if $a$ is associated to $b$, i.e., $a \sim b \cdot u \leftrightarrow a \sim b$.
associated_isUnit_mul_right_iff theorem
{N : Type*} [CommMonoid N] {a u b : N} (hu : IsUnit u) : Associated a (u * b) ↔ Associated a b
Full source 
theorem associated_isUnit_mul_right_iff {N : Type*} [CommMonoid N] {a u b : N} (hu : IsUnit u) :
    AssociatedAssociated a (u * b) ↔ Associated a b :=
  Associated.comm.trans <| (associated_isUnit_mul_left_iff hu).trans Associated.comm
Right Multiplication by Unit Preserves Association in Commutative Monoid: $a \sim u \cdot b \leftrightarrow a \sim b$
Informal description
Let $M$ be a commutative monoid, and let $a, b, u \in M$ with $u$ being a unit. Then $a$ is associated to $u \cdot b$ if and only if $a$ is associated to $b$, i.e., $a \sim u \cdot b \leftrightarrow a \sim b$.
associated_mul_unit_left_iff theorem
{N : Type*} [Monoid N] {a b : N} {u : Units N} : Associated (a * u) b ↔ Associated a b
Full source 
@[simp]
theorem associated_mul_unit_left_iff {N : Type*} [Monoid N] {a b : N} {u : Units N} :
    AssociatedAssociated (a * u) b ↔ Associated a b :=
  associated_mul_isUnit_left_iff u.isUnit
Left Multiplication by Unit Preserves Association Equivalence
Informal description
Let $M$ be a monoid and let $a, b \in M$ and $u$ be a unit in $M$. Then the element $a \cdot u$ is associated to $b$ if and only if $a$ is associated to $b$, i.e., $a \cdot u \sim b \leftrightarrow a \sim b$.
associated_unit_mul_left_iff theorem
{N : Type*} [CommMonoid N] {a b : N} {u : Units N} : Associated (↑u * a) b ↔ Associated a b
Full source 
@[simp]
theorem associated_unit_mul_left_iff {N : Type*} [CommMonoid N] {a b : N} {u : Units N} :
    AssociatedAssociated (↑u * a) b ↔ Associated a b :=
  associated_isUnit_mul_left_iff u.isUnit
Left multiplication by unit preserves association equivalence in commutative monoid
Informal description
Let $M$ be a commutative monoid, and let $a, b \in M$ and $u$ be a unit in $M$. Then the element $u \cdot a$ is associated to $b$ if and only if $a$ is associated to $b$, i.e., $u \cdot a \sim b \leftrightarrow a \sim b$.
associated_mul_unit_right_iff theorem
{N : Type*} [Monoid N] {a b : N} {u : Units N} : Associated a (b * u) ↔ Associated a b
Full source 
@[simp]
theorem associated_mul_unit_right_iff {N : Type*} [Monoid N] {a b : N} {u : Units N} :
    AssociatedAssociated a (b * u) ↔ Associated a b :=
  associated_mul_isUnit_right_iff u.isUnit
Right Multiplication by Unit Preserves Association Equivalence
Informal description
Let $M$ be a monoid and let $a, b \in M$ and $u$ be a unit in $M$. Then $a$ is associated to $b \cdot u$ if and only if $a$ is associated to $b$, i.e., $a \sim b \cdot u \leftrightarrow a \sim b$.
associated_unit_mul_right_iff theorem
{N : Type*} [CommMonoid N] {a b : N} {u : Units N} : Associated a (↑u * b) ↔ Associated a b
Full source 
@[simp]
theorem associated_unit_mul_right_iff {N : Type*} [CommMonoid N] {a b : N} {u : Units N} :
    AssociatedAssociated a (↑u * b) ↔ Associated a b :=
  associated_isUnit_mul_right_iff u.isUnit
Right Multiplication by Unit Preserves Association in Commutative Monoid: $a \sim u \cdot b \leftrightarrow a \sim b$
Informal description
Let $M$ be a commutative monoid, and let $a, b \in M$ with $u$ being a unit in $M$. Then $a$ is associated to $u \cdot b$ if and only if $a$ is associated to $b$, i.e., $a \sim u \cdot b \leftrightarrow a \sim b$.
Associated.mul_left theorem
[Monoid M] (a : M) {b c : M} (h : b ~ᵤ c) : a * b ~ᵤ a * c
Full source 
theorem Associated.mul_left [Monoid M] (a : M) {b c : M} (h : b ~ᵤ c) : a * b ~ᵤ a * c := by
  obtain ⟨d, rfl⟩ := h; exact ⟨d, mul_assoc _ _ _⟩
Left Multiplication Preserves Associated Elements in a Monoid
Informal description
Let $M$ be a monoid and let $a, b, c \in M$ such that $b$ and $c$ are associated (denoted $b \sim c$). Then $a \cdot b$ and $a \cdot c$ are also associated, i.e., $a \cdot b \sim a \cdot c$.
Associated.mul_right theorem
[CommMonoid M] {a b : M} (h : a ~ᵤ b) (c : M) : a * c ~ᵤ b * c
Full source 
theorem Associated.mul_right [CommMonoid M] {a b : M} (h : a ~ᵤ b) (c : M) : a * c ~ᵤ b * c := by
  obtain ⟨d, rfl⟩ := h; exact ⟨d, mul_right_comm _ _ _⟩
Right Multiplication Preserves Associated Elements in a Commutative Monoid
Informal description
Let $M$ be a commutative monoid. For any elements $a, b, c \in M$, if $a$ and $b$ are associated (i.e., $a \sim b$), then $a \cdot c$ and $b \cdot c$ are also associated (i.e., $a \cdot c \sim b \cdot c$).
Associated.mul_mul theorem
[CommMonoid M] {a₁ a₂ b₁ b₂ : M} (h₁ : a₁ ~ᵤ b₁) (h₂ : a₂ ~ᵤ b₂) : a₁ * a₂ ~ᵤ b₁ * b₂
Full source 
theorem Associated.mul_mul [CommMonoid M] {a₁ a₂ b₁ b₂ : M}
    (h₁ : a₁ ~ᵤ b₁) (h₂ : a₂ ~ᵤ b₂) : a₁ * a₂ ~ᵤ b₁ * b₂ := (h₁.mul_right _).trans (h₂.mul_left _)
Product of Associated Elements in a Commutative Monoid is Associated
Informal description
Let $M$ be a commutative monoid. For any elements $a₁, a₂, b₁, b₂ \in M$, if $a₁$ is associated to $b₁$ and $a₂$ is associated to $b₂$, then the product $a₁ \cdot a₂$ is associated to the product $b₁ \cdot b₂$, i.e., $a₁ \cdot a₂ \sim b₁ \cdot b₂$.
Associated.pow_pow theorem
[CommMonoid M] {a b : M} {n : ℕ} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n
Full source 
theorem Associated.pow_pow [CommMonoid M] {a b : M} {n : ℕ} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n := by
  induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert h.mul_mul ih <;> rw [pow_succ']
Powers of Associated Elements Remain Associated in a Commutative Monoid
Informal description
Let $M$ be a commutative monoid. For any elements $a, b \in M$ and any natural number $n$, if $a$ and $b$ are associated (i.e., $a \sim b$), then their $n$-th powers $a^n$ and $b^n$ are also associated (i.e., $a^n \sim b^n$).
Associated.dvd theorem
[Monoid M] {a b : M} : a ~ᵤ b → a ∣ b
Full source 
protected theorem Associated.dvd [Monoid M] {a b : M} : a ~ᵤ b → a ∣ b := fun ⟨u, hu⟩ =>
  ⟨u, hu.symm⟩
Associated Elements Imply Divisibility in Monoids
Informal description
For any elements $a$ and $b$ in a monoid $M$, if $a$ and $b$ are associated (i.e., $a \sim b$), then $a$ divides $b$ (i.e., $a \mid b$).
Associated.dvd' theorem
[Monoid M] {a b : M} (h : a ~ᵤ b) : b ∣ a
Full source 
protected theorem Associated.dvd' [Monoid M] {a b : M} (h : a ~ᵤ b) : b ∣ a :=
  h.symm.dvd
Associated Elements Imply Reverse Divisibility in Monoids
Informal description
For any elements $a$ and $b$ in a monoid $M$, if $a$ and $b$ are associated (i.e., $a \sim b$), then $b$ divides $a$ (i.e., $b \mid a$).
Associated.dvd_dvd theorem
[Monoid M] {a b : M} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a
Full source 
protected theorem Associated.dvd_dvd [Monoid M] {a b : M} (h : a ~ᵤ b) : a ∣ ba ∣ b ∧ b ∣ a :=
  ⟨h.dvd, h.symm.dvd⟩
Associated Elements are Mutually Divisible in a Monoid
Informal description
For any elements $a$ and $b$ in a monoid $M$, if $a$ and $b$ are associated (i.e., $a \sim b$), then $a$ divides $b$ and $b$ divides $a$ (i.e., $a \mid b$ and $b \mid a$).
associated_of_dvd_dvd theorem
[CancelMonoidWithZero M] {a b : M} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b
Full source 
theorem associated_of_dvd_dvd [CancelMonoidWithZero M] {a b : M} (hab : a ∣ b) (hba : b ∣ a) :
    a ~ᵤ b := by
  rcases hab with ⟨c, rfl⟩
  rcases hba with ⟨d, a_eq⟩
  by_cases ha0 : a = 0
  · simp_all
  have hac0 : a * c ≠ 0 := by
    intro con
    rw [con, zero_mul] at a_eq
    apply ha0 a_eq
  have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
  have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
  have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
  have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
  exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
Divisibility Implies Association in Cancellative Monoids with Zero
Informal description
Let $M$ be a cancellative monoid with zero. For any two elements $a, b \in M$, if $a$ divides $b$ and $b$ divides $a$, then $a$ and $b$ are associated, i.e., there exists a unit $u \in M^\times$ such that $a \cdot u = b$.
dvd_dvd_iff_associated theorem
[CancelMonoidWithZero M] {a b : M} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b
Full source 
theorem dvd_dvd_iff_associated [CancelMonoidWithZero M] {a b : M} : a ∣ ba ∣ b ∧ b ∣ aa ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
  ⟨fun ⟨h1, h2⟩ => associated_of_dvd_dvd h1 h2, Associated.dvd_dvd⟩
Divisibility and Association Equivalence in Cancellative Monoids with Zero
Informal description
Let $M$ be a cancellative monoid with zero. For any two elements $a, b \in M$, the following are equivalent: 1. $a$ divides $b$ and $b$ divides $a$ (i.e., $a \mid b$ and $b \mid a$), 2. $a$ and $b$ are associated (i.e., there exists a unit $u \in M^\times$ such that $a \cdot u = b$).
instDecidableRelAssociatedOfDvd instance
[CancelMonoidWithZero M] [DecidableRel ((· ∣ ·) : M → M → Prop)] : DecidableRel ((· ~ᵤ ·) : M → M → Prop)
Full source 
instance [CancelMonoidWithZero M] [DecidableRel ((· ∣ ·) : M → M → Prop)] :
    DecidableRel ((· ~ᵤ ·) : M → M → Prop) := fun _ _ => decidable_of_iff _ dvd_dvd_iff_associated
Decidability of the Associated Relation in Cancellative Monoids with Zero
Informal description
For any cancellative monoid with zero $M$ where the divisibility relation $(\cdot \mid \cdot)$ is decidable, the associated relation $(\cdot \sim \cdot)$ is also decidable.
Associated.dvd_iff_dvd_left theorem
[Monoid M] {a b c : M} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c
Full source 
theorem Associated.dvd_iff_dvd_left [Monoid M] {a b c : M} (h : a ~ᵤ b) : a ∣ ca ∣ c ↔ b ∣ c :=
  let ⟨_, hu⟩ := h
  hu ▸ Units.mul_right_dvd.symm
Associated Elements Have Equivalent Divisibility from the Left
Informal description
Let $M$ be a monoid and let $a, b, c \in M$. If $a$ and $b$ are associated (i.e., $a \sim b$), then $a$ divides $c$ if and only if $b$ divides $c$.
Associated.dvd_iff_dvd_right theorem
[Monoid M] {a b c : M} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c
Full source 
theorem Associated.dvd_iff_dvd_right [Monoid M] {a b c : M} (h : b ~ᵤ c) : a ∣ ba ∣ b ↔ a ∣ c :=
  let ⟨_, hu⟩ := h
  hu ▸ Units.dvd_mul_right.symm
Associated Elements Have Equivalent Divisibility from the Right
Informal description
Let $M$ be a monoid and let $a, b, c \in M$. If $b$ and $c$ are associated (i.e., $b \sim c$), then $a$ divides $b$ if and only if $a$ divides $c$.
Associated.ne_zero_iff theorem
[MonoidWithZero M] {a b : M} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0
Full source 
theorem Associated.ne_zero_iff [MonoidWithZero M] {a b : M} (h : a ~ᵤ b) : a ≠ 0a ≠ 0 ↔ b ≠ 0 :=
  not_congr h.eq_zero_iff
Nonzero Preservation under Associated Elements in a Monoid with Zero
Informal description
For any elements $a$ and $b$ in a monoid with zero $M$, if $a$ and $b$ are associated (i.e., $a \sim b$), then $a$ is nonzero if and only if $b$ is nonzero.
Associated.prime theorem
[CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) (hp : Prime p) : Prime q
Full source 
protected theorem Associated.prime [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) (hp : Prime p) :
    Prime q :=
  ⟨h.ne_zero_iff.1 hp.ne_zero,
    let ⟨u, hu⟩ := h
    ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
      hu ▸ by
        simp only [IsUnit.mul_iff, Units.isUnit, and_true, IsUnit.mul_right_dvd]
        intro a b
        exact hp.dvd_or_dvd⟩⟩
Primality is Preserved under Associated Elements in a Commutative Monoid with Zero
Informal description
Let $M$ be a commutative monoid with zero. For any elements $p$ and $q$ in $M$, if $p$ and $q$ are associated (i.e., $p \sim q$) and $p$ is prime, then $q$ is also prime.
prime_mul_iff theorem
[CancelCommMonoidWithZero M] {x y : M} : Prime (x * y) ↔ (Prime x ∧ IsUnit y) ∨ (IsUnit x ∧ Prime y)
Full source 
theorem prime_mul_iff [CancelCommMonoidWithZero M] {x y : M} :
    PrimePrime (x * y) ↔ (Prime x ∧ IsUnit y) ∨ (IsUnit x ∧ Prime y) := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases of_irreducible_mul h.irreducible with hx | hy
    · exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩
    · exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩
  · rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)
    · exact (associated_mul_unit_left x y hy).symm.prime hx
    · exact (associated_unit_mul_right y x hx).prime hy
Prime Product Characterization in Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any elements $x, y \in M$, the product $x \cdot y$ is prime if and only if either $x$ is prime and $y$ is a unit, or $x$ is a unit and $y$ is prime.
prime_pow_iff theorem
[CancelCommMonoidWithZero M] {p : M} {n : ℕ} : Prime (p ^ n) ↔ Prime p ∧ n = 1
Full source 
@[simp]
lemma prime_pow_iff [CancelCommMonoidWithZero M] {p : M} {n : ℕ} :
    PrimePrime (p ^ n) ↔ Prime p ∧ n = 1 := by
  refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
  suffices n = 1 by aesop
  rcases n with - | n
  · simp at hp
  · rw [Nat.succ.injEq]
    rw [pow_succ', prime_mul_iff] at hp
    rcases hp with ⟨hp, hpn⟩ | ⟨hp, hpn⟩
    · by_contra contra
      rw [isUnit_pow_iff contra] at hpn
      exact hp.not_unit hpn
    · exfalso
      exact hpn.not_unit (hp.pow n)
Prime Power Characterization: $p^n$ is prime iff $p$ is prime and $n=1$
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any element $p \in M$ and any natural number $n$, the power $p^n$ is prime if and only if $p$ is prime and $n = 1$.
Irreducible.dvd_iff theorem
[Monoid M] {x y : M} (hx : Irreducible x) : y ∣ x ↔ IsUnit y ∨ Associated x y
Full source 
theorem Irreducible.dvd_iff [Monoid M] {x y : M} (hx : Irreducible x) :
    y ∣ xy ∣ x ↔ IsUnit y ∨ Associated x y := by
  constructor
  · rintro ⟨z, hz⟩
    obtain (h|h) := hx.isUnit_or_isUnit hz
    · exact Or.inl h
    · rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)
  · rintro (hy|h)
    · exact hy.dvd
    · exact h.symm.dvd
Divisibility Condition for Irreducible Elements in a Monoid
Informal description
Let $M$ be a monoid and $x, y \in M$ with $x$ irreducible. Then $y$ divides $x$ if and only if either $y$ is a unit or $y$ is associated to $x$.
Irreducible.associated_of_dvd theorem
[Monoid M] {p q : M} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p ∣ q) : Associated p q
Full source 
theorem Irreducible.associated_of_dvd [Monoid M] {p q : M} (p_irr : Irreducible p)
    (q_irr : Irreducible q) (dvd : p ∣ q) : Associated p q :=
  ((q_irr.dvd_iff.mp dvd).resolve_left p_irr.not_isUnit).symm
Irreducible elements dividing each other are associated
Informal description
Let $M$ be a monoid and let $p, q \in M$ be irreducible elements. If $p$ divides $q$, then $p$ and $q$ are associated, i.e., there exists a unit $u \in M$ such that $p \cdot u = q$.
Irreducible.dvd_irreducible_iff_associated theorem
[Monoid M] {p q : M} (pp : Irreducible p) (qp : Irreducible q) : p ∣ q ↔ Associated p q
Full source 
theorem Irreducible.dvd_irreducible_iff_associated [Monoid M] {p q : M}
    (pp : Irreducible p) (qp : Irreducible q) : p ∣ qp ∣ q ↔ Associated p q :=
  ⟨Irreducible.associated_of_dvd pp qp, Associated.dvd⟩
Divisibility of Irreducible Elements is Equivalent to Being Associated
Informal description
Let $M$ be a monoid and let $p, q \in M$ be irreducible elements. Then $p$ divides $q$ if and only if $p$ and $q$ are associated, i.e., there exists a unit $u \in M$ such that $p \cdot u = q$.
Prime.associated_of_dvd theorem
[CancelCommMonoidWithZero M] {p q : M} (p_prime : Prime p) (q_prime : Prime q) (dvd : p ∣ q) : Associated p q
Full source 
theorem Prime.associated_of_dvd [CancelCommMonoidWithZero M] {p q : M} (p_prime : Prime p)
    (q_prime : Prime q) (dvd : p ∣ q) : Associated p q :=
  p_prime.irreducible.associated_of_dvd q_prime.irreducible dvd
Associated Primes in a Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any prime elements $p, q \in M$, if $p$ divides $q$, then $p$ and $q$ are associated, i.e., there exists a unit $u \in M$ such that $p \cdot u = q$.
Prime.dvd_prime_iff_associated theorem
[CancelCommMonoidWithZero M] {p q : M} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ Associated p q
Full source 
theorem Prime.dvd_prime_iff_associated [CancelCommMonoidWithZero M] {p q : M} (pp : Prime p)
    (qp : Prime q) : p ∣ qp ∣ q ↔ Associated p q :=
  pp.irreducible.dvd_irreducible_iff_associated qp.irreducible
Divisibility of Primes is Equivalent to Being Associated in a Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any prime elements $p, q \in M$, $p$ divides $q$ if and only if $p$ and $q$ are associated, i.e., there exists a unit $u \in M$ such that $p \cdot u = q$.
Associated.prime_iff theorem
[CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) : Prime p ↔ Prime q
Full source 
theorem Associated.prime_iff [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) : PrimePrime p ↔ Prime q :=
  ⟨h.prime, h.symm.prime⟩
Primality Equivalence for Associated Elements in a Commutative Monoid with Zero
Informal description
Let $M$ be a commutative monoid with zero. For any elements $p$ and $q$ in $M$ that are associated (i.e., $p \sim q$), $p$ is prime if and only if $q$ is prime.
Associated.isUnit theorem
[Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a → IsUnit b
Full source 
protected theorem Associated.isUnit [Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a → IsUnit b :=
  let ⟨u, hu⟩ := h
  fun ⟨v, hv⟩ => ⟨v * u, by simp [hv, hu.symm]⟩
Associated Elements Preserve Unit Property
Informal description
Let $M$ be a monoid and let $a, b \in M$ be associated elements (i.e., $a \sim b$). If $a$ is a unit, then $b$ is also a unit.
Associated.isUnit_iff theorem
[Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnit a ↔ IsUnit b
Full source 
theorem Associated.isUnit_iff [Monoid M] {a b : M} (h : a ~ᵤ b) : IsUnitIsUnit a ↔ IsUnit b :=
  ⟨h.isUnit, h.symm.isUnit⟩
Unit Property Equivalence for Associated Elements in a Monoid
Informal description
For any elements $a$ and $b$ in a monoid $M$ such that $a$ is associated to $b$ (i.e., $a \sim b$), the element $a$ is a unit if and only if $b$ is a unit.
Irreducible.isUnit_iff_not_associated_of_dvd theorem
[Monoid M] {x y : M} (hx : Irreducible x) (hy : y ∣ x) : IsUnit y ↔ ¬Associated x y
Full source 
theorem Irreducible.isUnit_iff_not_associated_of_dvd [Monoid M]
    {x y : M} (hx : Irreducible x) (hy : y ∣ x) : IsUnitIsUnit y ↔ ¬ Associated x y :=
  ⟨fun hy hxy => hx.1 (hxy.symm.isUnit hy), (hx.dvd_iff.mp hy).resolve_right⟩
Unit Criterion for Divisors of Irreducible Elements in a Monoid
Informal description
Let $M$ be a monoid and let $x, y \in M$ with $x$ irreducible and $y$ dividing $x$. Then $y$ is a unit if and only if $y$ is not associated to $x$.
Associated.irreducible theorem
[Monoid M] {p q : M} (h : p ~ᵤ q) (hp : Irreducible p) : Irreducible q
Full source 
protected theorem Associated.irreducible [Monoid M] {p q : M} (h : p ~ᵤ q) (hp : Irreducible p) :
    Irreducible q :=
  ⟨mt h.symm.isUnit hp.1,
    let ⟨u, hu⟩ := h
    fun a b hab =>
    have hpab : p = a * (b * (u⁻¹ : Mˣ)) :=
      calc
        p = p * u * (u⁻¹ : Mˣ) := by simp
        _ = _ := by rw [hu]; simp [hab, mul_assoc]

    (hp.isUnit_or_isUnit hpab).elim Or.inl fun ⟨v, hv⟩ => Or.inr ⟨v * u, by simp [hv]⟩⟩
Associated Elements Preserve Irreducibility
Informal description
Let $M$ be a monoid and let $p, q \in M$ be associated elements (i.e., $p \sim q$). If $p$ is irreducible, then $q$ is also irreducible.
Associated.irreducible_iff theorem
[Monoid M] {p q : M} (h : p ~ᵤ q) : Irreducible p ↔ Irreducible q
Full source 
protected theorem Associated.irreducible_iff [Monoid M] {p q : M} (h : p ~ᵤ q) :
    IrreducibleIrreducible p ↔ Irreducible q :=
  ⟨h.irreducible, h.symm.irreducible⟩
Irreducibility is Preserved Under Associated Elements
Informal description
Let $M$ be a monoid and let $p, q \in M$ be associated elements (i.e., $p \sim q$). Then $p$ is irreducible if and only if $q$ is irreducible.
Associated.of_mul_left theorem
[CancelCommMonoidWithZero M] {a b c d : M} (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d
Full source 
theorem Associated.of_mul_left [CancelCommMonoidWithZero M] {a b c d : M} (h : a * b ~ᵤ c * d)
    (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
  let ⟨u, hu⟩ := h
  let ⟨v, hv⟩ := Associated.symm h₁
  ⟨u * (v : Mˣ),
    mul_left_cancel₀ ha
      (by
        rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]
        simp [hv.symm, mul_assoc, mul_comm, mul_left_comm])⟩
Left Cancellation of Associated Elements in a Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any elements $a, b, c, d \in M$ such that $a \cdot b$ is associated to $c \cdot d$ (i.e., $a \cdot b \sim c \cdot d$), if $a$ is associated to $c$ (i.e., $a \sim c$) and $a \neq 0$, then $b$ is associated to $d$ (i.e., $b \sim d$).
Associated.of_mul_right theorem
[CancelCommMonoidWithZero M] {a b c d : M} : a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Full source 
theorem Associated.of_mul_right [CancelCommMonoidWithZero M] {a b c d : M} :
    a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c := by
  rw [mul_comm a, mul_comm c]; exact Associated.of_mul_left
Right Cancellation of Associated Elements in a Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any elements $a, b, c, d \in M$ such that $a \cdot b$ is associated to $c \cdot d$ (i.e., $a \cdot b \sim c \cdot d$), if $b$ is associated to $d$ (i.e., $b \sim d$) and $b \neq 0$, then $a$ is associated to $c$ (i.e., $a \sim c$).
Associated.of_pow_associated_of_prime theorem
[CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂
Full source 
theorem Associated.of_pow_associated_of_prime [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ}
    (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂ := by
  have : p₁ ∣ p₂ ^ k₂ := by
    rw [← h.dvd_iff_dvd_right]
    apply dvd_pow_self _ hk₁.ne'
  rw [← hp₁.dvd_prime_iff_associated hp₂]
  exact hp₁.dvd_of_dvd_pow this
Associated Powers of Primes Imply Associated Primes
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any prime elements $p₁, p₂ \in M$ and positive integers $k₁, k₂ \in \mathbb{N}$, if $p₁^{k₁}$ is associated to $p₂^{k₂}$ (i.e., there exists a unit $u$ such that $p₁^{k₁} \cdot u = p₂^{k₂}$), then $p₁$ is associated to $p₂$.
Associated.of_pow_associated_of_prime' theorem
[CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₂ : 0 < k₂) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂
Full source 
theorem Associated.of_pow_associated_of_prime' [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ}
    (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₂ : 0 < k₂) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂ :=
  (h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm
Associated Powers of Primes Imply Associated Primes (Symmetric Version)
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any prime elements $p₁, p₂ \in M$ and positive integers $k₁, k₂ \in \mathbb{N}$ with $k₂ > 0$, if $p₁^{k₁}$ is associated to $p₂^{k₂}$ (i.e., there exists a unit $u$ such that $p₁^{k₁} \cdot u = p₂^{k₂}$), then $p₁$ is associated to $p₂$.
Irreducible.isRelPrime_iff_not_dvd theorem
[Monoid M] {p n : M} (hp : Irreducible p) : IsRelPrime p n ↔ ¬p ∣ n
Full source 
/-- See also `Irreducible.coprime_iff_not_dvd`. -/
lemma Irreducible.isRelPrime_iff_not_dvd [Monoid M] {p n : M} (hp : Irreducible p) :
    IsRelPrimeIsRelPrime p n ↔ ¬ p ∣ n := by
  refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
  contrapose! hpn
  suffices Associated p d from this.dvd.trans hdn
  exact (hp.dvd_iff.mp hdp).resolve_left hpn
Irreducible elements are relatively prime iff they do not divide each other
Informal description
Let $M$ be a monoid and $p, n \in M$ with $p$ irreducible. Then $p$ and $n$ are relatively prime if and only if $p$ does not divide $n$.
Irreducible.dvd_or_isRelPrime theorem
[Monoid M] {p n : M} (hp : Irreducible p) : p ∣ n ∨ IsRelPrime p n
Full source 
lemma Irreducible.dvd_or_isRelPrime [Monoid M] {p n : M} (hp : Irreducible p) :
    p ∣ np ∣ n ∨ IsRelPrime p n := Classical.or_iff_not_imp_left.mpr hp.isRelPrime_iff_not_dvd.2
Irreducible Elements Either Divide or Are Relatively Prime
Informal description
Let $M$ be a monoid and $p, n \in M$ with $p$ irreducible. Then either $p$ divides $n$ or $p$ and $n$ are relatively prime.
associated_iff_eq theorem
{x y : M} : x ~ᵤ y ↔ x = y
Full source 
theorem associated_iff_eq {x y : M} : x ~ᵤ yx ~ᵤ y ↔ x = y := by
  constructor
  · rintro ⟨c, rfl⟩
    rw [units_eq_one c, Units.val_one, mul_one]
  · rintro rfl
    rfl
Associated Elements are Equal in Subsingleton Unit Monoid
Informal description
For any elements $x$ and $y$ in a monoid $M$ where the group of units $M^\times$ is a subsingleton, $x$ and $y$ are associated if and only if they are equal, i.e., $x \sim y \leftrightarrow x = y$.
associated_eq_eq theorem
: (Associated : M → M → Prop) = Eq
Full source 
theorem associated_eq_eq : (Associated : M → M → Prop) = Eq := by
  ext
  rw [associated_iff_eq]
Associated Relation Equals Equality in Subsingleton Unit Monoid
Informal description
In a monoid $M$ where the group of units $M^\times$ is a subsingleton, the associated relation $\sim$ coincides with equality, i.e., $\sim = \text{Eq}$.
prime_dvd_prime_iff_eq theorem
{M : Type*} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ p = q
Full source 
theorem prime_dvd_prime_iff_eq {M : Type*} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p q : M}
    (pp : Prime p) (qp : Prime q) : p ∣ qp ∣ q ↔ p = q := by
  rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]
Divisibility of Primes is Equivalent to Equality in Monoid with Unique Units
Informal description
Let $M$ be a cancelative commutative monoid with zero such that the group of units $M^\times$ is a subsingleton. For any prime elements $p, q \in M$, $p$ divides $q$ if and only if $p = q$.
Associates abbrev
(M : Type*) [Monoid M] : Type _
Full source 
/-- The quotient of a monoid by the `Associated` relation. Two elements `x` and `y`
  are associated iff there is a unit `u` such that `x * u = y`. There is a natural
  monoid structure on `Associates M`. -/
abbrev Associates (M : Type*) [Monoid M] : Type _ :=
  Quotient (Associated.setoid M)
Quotient Monoid of Associated Elements
Informal description
Given a monoid $M$, the type `Associates M` is the quotient of $M$ by the equivalence relation of being *associated elements*, where two elements $x, y \in M$ are associated if there exists a unit $u \in M$ such that $x \cdot u = y$. This quotient inherits a natural monoid structure from $M$.
Associates.mk abbrev
{M : Type*} [Monoid M] (a : M) : Associates M
Full source 
/-- The canonical quotient map from a monoid `M` into the `Associates` of `M` -/
protected abbrev mk {M : Type*} [Monoid M] (a : M) : Associates M :=
  ⟦a⟧
Canonical Quotient Map to Associates Monoid
Informal description
Given a monoid $M$ and an element $a \in M$, the function $\text{Associates.mk}$ maps $a$ to its equivalence class in the quotient monoid $\text{Associates } M$, where elements are considered equivalent if they are associated (i.e., differ by multiplication by a unit).
Associates.instInhabited instance
[Monoid M] : Inhabited (Associates M)
Full source 
instance [Monoid M] : Inhabited (Associates M) :=
  ⟨⟦1⟧⟩
Inhabited Quotient of Associated Elements in a Monoid
Informal description
For any monoid $M$, the quotient type $\text{Associates } M$ of associated elements is inhabited.
Associates.mk_eq_mk_iff_associated theorem
[Monoid M] {a b : M} : Associates.mk a = Associates.mk b ↔ a ~ᵤ b
Full source 
theorem mk_eq_mk_iff_associated [Monoid M] {a b : M} : Associates.mkAssociates.mk a = Associates.mk b ↔ a ~ᵤ b :=
  Iff.intro Quotient.exact Quot.sound
Equality in Associates Monoid iff Elements are Associated
Informal description
For any elements $a$ and $b$ in a monoid $M$, the equivalence classes of $a$ and $b$ in the quotient monoid $\text{Associates } M$ are equal if and only if $a$ and $b$ are associated, i.e., there exists a unit $u \in M$ such that $a \cdot u = b$.
Associates.quotient_mk_eq_mk theorem
[Monoid M] (a : M) : ⟦a⟧ = Associates.mk a
Full source 
theorem quotient_mk_eq_mk [Monoid M] (a : M) : ⟦a⟧ = Associates.mk a :=
  rfl
Equivalence Class in Associates Monoid Equals Canonical Image
Informal description
For any monoid $M$ and any element $a \in M$, the equivalence class of $a$ in the quotient by the associated elements relation is equal to the canonical image of $a$ in the `Associates` monoid, i.e., $\llbracket a \rrbracket = \text{Associates.mk}(a)$.
Associates.quot_mk_eq_mk theorem
[Monoid M] (a : M) : Quot.mk Setoid.r a = Associates.mk a
Full source 
theorem quot_mk_eq_mk [Monoid M] (a : M) : Quot.mk Setoid.r a = Associates.mk a :=
  rfl
Equivalence Class of Associated Elements Equals Canonical Quotient Image
Informal description
For any element $a$ in a monoid $M$, the equivalence class of $a$ under the associated elements relation is equal to the image of $a$ under the canonical quotient map to the monoid of associates.
Associates.quot_out theorem
[Monoid M] (a : Associates M) : Associates.mk (Quot.out a) = a
Full source 
@[simp]
theorem quot_out [Monoid M] (a : Associates M) : Associates.mk (Quot.out a) = a := by
  rw [← quot_mk_eq_mk, Quot.out_eq]
Canonical Quotient Map Preserves Representative Selection in Associates Monoid
Informal description
For any element $a$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the canonical quotient map applied to a representative of $a$ (selected via $\text{Quot.out}$) equals $a$ itself.
Associates.mk_quot_out theorem
[Monoid M] (a : M) : Quot.out (Associates.mk a) ~ᵤ a
Full source 
theorem mk_quot_out [Monoid M] (a : M) : Quot.outQuot.out (Associates.mk a) ~ᵤ a := by
  rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]
Representative in Associates Monoid is Associated to Original Element
Informal description
For any element $a$ in a monoid $M$, the representative selected from the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is associated to $a$. That is, there exists a unit $u \in M$ such that $\text{Quot.out}(\text{Associates.mk}(a)) \cdot u = a$.
Associates.forall_associated theorem
[Monoid M] {p : Associates M → Prop} : (∀ a, p a) ↔ ∀ a, p (Associates.mk a)
Full source 
theorem forall_associated [Monoid M] {p : Associates M → Prop} :
    (∀ a, p a) ↔ ∀ a, p (Associates.mk a) :=
  Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h
Universal Property of the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$ and any predicate $p$ on the quotient monoid $\text{Associates}\, M$, the statement that $p$ holds for all elements of $\text{Associates}\, M$ is equivalent to the statement that $p$ holds for the image of every element of $M$ under the canonical quotient map $\text{Associates.mk}$.
Associates.mk_surjective theorem
[Monoid M] : Function.Surjective (@Associates.mk M _)
Full source 
theorem mk_surjective [Monoid M] : Function.Surjective (@Associates.mk M _) :=
  forall_associated.2 fun a => ⟨a, rfl⟩
Surjectivity of the Canonical Quotient Map to Associates Monoid
Informal description
For any monoid $M$, the canonical quotient map $\text{Associates.mk} : M \to \text{Associates}\, M$ is surjective. That is, every element of the quotient monoid $\text{Associates}\, M$ is the image of some element of $M$ under $\text{Associates.mk}$.
Associates.instOne instance
[Monoid M] : One (Associates M)
Full source 
instance [Monoid M] : One (Associates M) :=
  ⟨⟦1⟧⟩
Identity Element in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$, the quotient type $\text{Associates}\, M$ of associated elements has a distinguished element $1$ inherited from the multiplicative identity of $M$.
Associates.mk_one theorem
[Monoid M] : Associates.mk (1 : M) = 1
Full source 
@[simp]
theorem mk_one [Monoid M] : Associates.mk (1 : M) = 1 :=
  rfl
Identity Preservation in the Quotient Monoid of Associated Elements
Informal description
In any monoid $M$, the equivalence class of the multiplicative identity $1$ under the associated elements relation is equal to the identity element in the quotient monoid $\text{Associates}\, M$, i.e., $\text{Associates.mk}(1) = 1$.
Associates.one_eq_mk_one theorem
[Monoid M] : (1 : Associates M) = Associates.mk 1
Full source 
theorem one_eq_mk_one [Monoid M] : (1 : Associates M) = Associates.mk 1 :=
  rfl
Identity in Associates Quotient Equals Class of Identity
Informal description
In the quotient monoid of associated elements of a monoid $M$, the multiplicative identity $1$ is equal to the equivalence class of the multiplicative identity of $M$, i.e., $1 = \text{Associates.mk}(1)$.
Associates.mk_eq_one theorem
[Monoid M] {a : M} : Associates.mk a = 1 ↔ IsUnit a
Full source 
@[simp]
theorem mk_eq_one [Monoid M] {a : M} : Associates.mkAssociates.mk a = 1 ↔ IsUnit a := by
  rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]
Equivalence Class of $a$ is Identity in Associates Monoid iff $a$ is a Unit
Informal description
For any element $a$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is equal to the identity element $1$ if and only if $a$ is a unit in $M$.
Associates.instBot instance
[Monoid M] : Bot (Associates M)
Full source 
instance [Monoid M] : Bot (Associates M) :=
  ⟨1⟩
Bottom Element in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$, the quotient type $\text{Associates}\, M$ of associated elements has a distinguished bottom element $\bot$ inherited from the multiplicative identity of $M$.
Associates.bot_eq_one theorem
[Monoid M] : (⊥ : Associates M) = 1
Full source 
theorem bot_eq_one [Monoid M] : (⊥ : Associates M) = 1 :=
  rfl
Bottom Element Equals Identity in Quotient Monoid of Associated Elements
Informal description
In the quotient monoid of associated elements of a monoid $M$, the bottom element $\bot$ is equal to the multiplicative identity $1$.
Associates.exists_rep theorem
[Monoid M] (a : Associates M) : ∃ a0 : M, Associates.mk a0 = a
Full source 
theorem exists_rep [Monoid M] (a : Associates M) : ∃ a0 : M, Associates.mk a0 = a :=
  Quot.exists_rep a
Existence of Representatives in the Quotient Monoid of Associated Elements
Informal description
For any element $a$ in the quotient monoid $\text{Associates } M$ of associated elements of a monoid $M$, there exists an element $a_0 \in M$ such that the equivalence class of $a_0$ under the associated relation is equal to $a$. In other words, every element in the quotient has a representative in the original monoid.
Associates.instUniqueOfSubsingleton instance
[Monoid M] [Subsingleton M] : Unique (Associates M)
Full source 
instance [Monoid M] [Subsingleton M] :
    Unique (Associates M) where
  default := 1
  uniq := forall_associated.2 fun _ ↦ mk_eq_one.2 <| isUnit_of_subsingleton _
Uniqueness of the Quotient Monoid for Subsingleton Monoids
Informal description
For any monoid $M$ that is a subsingleton (i.e., has at most one element), the quotient monoid $\text{Associates}\, M$ of associated elements has a unique element.
Associates.mk_injective theorem
[Monoid M] [Subsingleton Mˣ] : Function.Injective (@Associates.mk M _)
Full source 
theorem mk_injective [Monoid M] [Subsingleton Mˣ] : Function.Injective (@Associates.mk M _) :=
  fun _ _ h => associated_iff_eq.mp (Associates.mk_eq_mk_iff_associated.mp h)
Injectivity of the Quotient Map to Associates Monoid for Subsingleton Units
Informal description
For a monoid $M$ where the group of units $M^\times$ is a subsingleton, the canonical quotient map $\text{Associates.mk} : M \to \text{Associates } M$ is injective. In other words, if $\text{Associates.mk}(x) = \text{Associates.mk}(y)$ for $x, y \in M$, then $x = y$.
Associates.instMul instance
: Mul (Associates M)
Full source 
instance instMul : Mul (Associates M) :=
  ⟨Quotient.map₂ (· * ·) fun _ _ h₁ _ _ h₂ ↦ h₁.mul_mul h₂⟩
Multiplication on the Quotient Monoid of Associated Elements
Informal description
The quotient monoid `Associates M` of a monoid $M$ by the associated elements equivalence relation has a multiplication operation defined by lifting the multiplication from $M$. Specifically, for any two equivalence classes $[x]$ and $[y]$ in `Associates M`, their product is defined as $[x \cdot y]$.
Associates.mk_mul_mk theorem
{x y : M} : Associates.mk x * Associates.mk y = Associates.mk (x * y)
Full source 
theorem mk_mul_mk {x y : M} : Associates.mk x * Associates.mk y = Associates.mk (x * y) :=
  rfl
Multiplication of Associated Elements in Quotient Monoid: $[x] \cdot [y] = [x \cdot y]$
Informal description
For any elements $x$ and $y$ in a monoid $M$, the product of their equivalence classes in the quotient monoid $\text{Associates } M$ is equal to the equivalence class of their product in $M$, i.e., $[x] \cdot [y] = [x \cdot y]$.
Associates.instCommMonoid instance
: CommMonoid (Associates M)
Full source 
instance instCommMonoid : CommMonoid (Associates M) where
  one := 1
  mul := (· * ·)
  mul_one a' := Quotient.inductionOn a' fun a => show ⟦a * 1⟧ = ⟦a⟧ by simp
  one_mul a' := Quotient.inductionOn a' fun a => show ⟦1 * a⟧ = ⟦a⟧ by simp
  mul_assoc a' b' c' :=
    Quotient.inductionOn₃ a' b' c' fun a b c =>
      show ⟦a * b * c⟧ = ⟦a * (b * c)⟧ by rw [mul_assoc]
  mul_comm a' b' :=
    Quotient.inductionOn₂ a' b' fun a b => show ⟦a * b⟧ = ⟦b * a⟧ by rw [mul_comm]
Commutative Monoid Structure on the Quotient of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements is a commutative monoid. The multiplication operation on $\text{Associates}\, M$ is commutative and inherits the monoid structure from $M$.
Associates.mkMonoidHom definition
: M →* Associates M
Full source 
/-- `Associates.mk` as a `MonoidHom`. -/
protected def mkMonoidHom : M →* Associates M where
  toFun := Associates.mk
  map_one' := mk_one
  map_mul' _ _ := mk_mul_mk
Canonical monoid homomorphism to quotient of associated elements
Informal description
The function `Associates.mkMonoidHom` is a monoid homomorphism from a monoid $M$ to its quotient monoid of associated elements $\text{Associates}\, M$. It maps each element $a \in M$ to its equivalence class $[a]$ in the quotient, preserves the multiplicative identity (i.e., $[1] = 1$), and satisfies $[x \cdot y] = [x] \cdot [y]$ for all $x, y \in M$.
Associates.mkMonoidHom_apply theorem
(a : M) : Associates.mkMonoidHom a = Associates.mk a
Full source 
@[simp]
theorem mkMonoidHom_apply (a : M) : Associates.mkMonoidHom a = Associates.mk a :=
  rfl
Canonical Homomorphism Maps Element to its Associated Class
Informal description
For any element $a$ in a monoid $M$, the monoid homomorphism $\text{Associates.mkMonoidHom}$ maps $a$ to its equivalence class $[a]$ in the quotient monoid $\text{Associates}\, M$.
Associates.associated_map_mk theorem
{f : Associates M →* M} (hinv : Function.RightInverse f Associates.mk) (a : M) : a ~ᵤ f (Associates.mk a)
Full source 
theorem associated_map_mk {f : AssociatesAssociates M →* M} (hinv : Function.RightInverse f Associates.mk)
    (a : M) : a ~ᵤ f (Associates.mk a) :=
  Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm
Associated Elements under Right Inverse of Quotient Map
Informal description
Let $M$ be a monoid and $f \colon \text{Associates}\, M \to M$ be a monoid homomorphism that is a right inverse of the canonical quotient map $\text{Associates.mk} \colon M \to \text{Associates}\, M$. Then for any element $a \in M$, $a$ is associated to $f(\text{Associates.mk}\, a)$, i.e., there exists a unit $u \in M$ such that $a \cdot u = f(\text{Associates.mk}\, a)$.
Associates.mk_pow theorem
(a : M) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n
Full source 
theorem mk_pow (a : M) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n := by
  induction n <;> simp [*, pow_succ, Associates.mk_mul_mk.symm]
Power of Associated Elements: $[a^n] = [a]^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the equivalence class of $a^n$ in the quotient monoid $\text{Associates}\, M$ is equal to the $n$-th power of the equivalence class of $a$, i.e., $[a^n] = [a]^n$.
Associates.dvd_eq_le theorem
: ((· ∣ ·) : Associates M → Associates M → Prop) = (· ≤ ·)
Full source 
theorem dvd_eq_le : ((· ∣ ·) : Associates M → Associates M → Prop) = (· ≤ ·) :=
  rfl
Divisibility as Preorder in the Quotient of Associated Elements
Informal description
In the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the divisibility relation $\mid$ coincides with the preorder relation $\leq$ inherited from $M$.
Associates.uniqueUnits instance
: Unique (Associates M)ˣ
Full source 
instance uniqueUnits : Unique (Associates M)ˣ where
  uniq := by
    rintro ⟨a, b, hab, hba⟩
    revert hab hba
    exact Quotient.inductionOn₂ a b <| fun a b hab hba ↦ Units.ext <| Quotient.sound <|
      associated_one_of_associated_mul_one <| Quotient.exact hab
Uniqueness of the Unit in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$, the group of units in the quotient monoid $\text{Associates}\, M$ of associated elements has exactly one element, which is the equivalence class of the multiplicative identity $1$.
Associates.coe_unit_eq_one theorem
(u : (Associates M)ˣ) : (u : Associates M) = 1
Full source 
@[simp]
theorem coe_unit_eq_one (u : (Associates M)ˣ) : (u : Associates M) = 1 := by
  simp [eq_iff_true_of_subsingleton]
Image of Unit in Quotient Monoid Equals One
Informal description
For any unit $u$ in the group of units of the quotient monoid $\text{Associates}\, M$, the image of $u$ under the canonical map to $\text{Associates}\, M$ is equal to the multiplicative identity $1$.
Associates.isUnit_iff_eq_one theorem
(a : Associates M) : IsUnit a ↔ a = 1
Full source 
theorem isUnit_iff_eq_one (a : Associates M) : IsUnitIsUnit a ↔ a = 1 :=
  Iff.intro (fun ⟨_, h⟩ => h ▸ coe_unit_eq_one _) fun h => h.symm ▸ isUnit_one
Characterization of Units in the Quotient Monoid: $a$ is a unit $\iff$ $a = 1$
Informal description
For any element $a$ in the quotient monoid $\text{Associates}\, M$ of associated elements, $a$ is a unit if and only if $a$ is equal to the multiplicative identity $1$.
Associates.isUnit_mk theorem
{a : M} : IsUnit (Associates.mk a) ↔ IsUnit a
Full source 
theorem isUnit_mk {a : M} : IsUnitIsUnit (Associates.mk a) ↔ IsUnit a :=
  calc
    IsUnit (Associates.mk a) ↔ a ~ᵤ 1 := by
      rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
    _ ↔ IsUnit a := associated_one_iff_isUnit
Unit Characterization in Associates Quotient: $\text{IsUnit}(\text{Associates.mk}(a)) \leftrightarrow \text{IsUnit}(a)$
Informal description
For any element $a$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is a unit if and only if $a$ itself is a unit in $M$.
Associates.mul_mono theorem
{a b c d : Associates M} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d
Full source 
theorem mul_mono {a b c d : Associates M} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d :=
  let ⟨x, hx⟩ := h₁
  let ⟨y, hy⟩ := h₂
  ⟨x * y, by simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]⟩
Monotonicity of Multiplication in the Quotient Monoid of Associated Elements
Informal description
For any elements $a, b, c, d$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, if $a \leq b$ and $c \leq d$ in the divisibility preorder, then $a \cdot c \leq b \cdot d$.
Associates.one_le theorem
{a : Associates M} : 1 ≤ a
Full source 
theorem one_le {a : Associates M} : 1 ≤ a :=
  Dvd.intro _ (one_mul a)
Identity Element is Least in Divisibility Preorder on Associated Elements Quotient
Informal description
For any element $a$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the identity element $1$ is less than or equal to $a$ with respect to the divisibility preorder.
Associates.le_mul_right theorem
{a b : Associates M} : a ≤ a * b
Full source 
theorem le_mul_right {a b : Associates M} : a ≤ a * b :=
  ⟨b, rfl⟩
Right Multiplication Preserves Divisibility in Quotient Monoid of Associated Elements
Informal description
For any elements $a, b$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the inequality $a \leq a \cdot b$ holds, where $\leq$ is the divisibility preorder on $\text{Associates}\, M$.
Associates.le_mul_left theorem
{a b : Associates M} : a ≤ b * a
Full source 
theorem le_mul_left {a b : Associates M} : a ≤ b * a := by rw [mul_comm]; exact le_mul_right
Left Multiplication Preserves Divisibility in Quotient Monoid of Associated Elements
Informal description
For any elements $a, b$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the inequality $a \leq b \cdot a$ holds, where $\leq$ is the divisibility preorder on $\text{Associates}\, M$.
Associates.instOrderBot instance
: OrderBot (Associates M)
Full source 
instance instOrderBot : OrderBot (Associates M) where
  bot := 1
  bot_le _ := one_le
Bottom Element in the Divisibility Preorder on Associated Elements Quotient
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements has a bottom element with respect to the divisibility preorder, namely the equivalence class of the identity element $1 \in M$.
Associates.mk_dvd_mk theorem
{a b : M} : Associates.mk a ∣ Associates.mk b ↔ a ∣ b
Full source 
@[simp]
theorem mk_dvd_mk {a b : M} : Associates.mkAssociates.mk a ∣ Associates.mk bAssociates.mk a ∣ Associates.mk b ↔ a ∣ b := by
  simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := b)]
  constructor
  · rintro ⟨x, u, rfl⟩
    exact ⟨_, mul_assoc ..⟩
  · rintro ⟨c, rfl⟩
    use c
Divisibility in Quotient Monoid of Associated Elements Reflects Original Monoid Divisibility
Informal description
For any elements $a$ and $b$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ divides the equivalence class of $b$ if and only if $a$ divides $b$ in $M$. In other words, $\text{Associates.mk}\, a \mid \text{Associates.mk}\, b \leftrightarrow a \mid b$.
Associates.dvd_of_mk_le_mk theorem
{a b : M} : Associates.mk a ≤ Associates.mk b → a ∣ b
Full source 
theorem dvd_of_mk_le_mk {a b : M} : Associates.mk a ≤ Associates.mk b → a ∣ b :=
  mk_dvd_mk.mp
Divisibility in Original Monoid from Quotient Preorder
Informal description
For any elements $a$ and $b$ in a monoid $M$, if the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is less than or equal to the equivalence class of $b$ under the divisibility preorder, then $a$ divides $b$ in $M$.
Associates.mk_le_mk_of_dvd theorem
{a b : M} : a ∣ b → Associates.mk a ≤ Associates.mk b
Full source 
theorem mk_le_mk_of_dvd {a b : M} : a ∣ b → Associates.mk a ≤ Associates.mk b :=
  mk_dvd_mk.mpr
Divisibility Implies Preorder Relation in Quotient Monoid of Associated Elements
Informal description
For any elements $a$ and $b$ in a monoid $M$, if $a$ divides $b$ in $M$, then the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is less than or equal to the equivalence class of $b$ under the divisibility preorder. In other words, $a \mid b$ implies $\text{Associates.mk}\, a \leq \text{Associates.mk}\, b$.
Associates.mk_le_mk_iff_dvd theorem
{a b : M} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b
Full source 
theorem mk_le_mk_iff_dvd {a b : M} : Associates.mkAssociates.mk a ≤ Associates.mk b ↔ a ∣ b := mk_dvd_mk
Divisibility in Quotient Monoid of Associated Elements Reflects Original Monoid Divisibility
Informal description
For any elements $a$ and $b$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is less than or equal to the equivalence class of $b$ if and only if $a$ divides $b$ in $M$. That is, $\text{Associates.mk}\, a \leq \text{Associates.mk}\, b \leftrightarrow a \mid b$.
Associates.isPrimal_mk theorem
{a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a
Full source 
@[simp]
theorem isPrimal_mk {a : M} : IsPrimalIsPrimal (Associates.mk a) ↔ IsPrimal a := by
  simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]
  constructor <;> intro h b c dvd <;> obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
  · obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
    exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
  · exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩
Primality is Preserved in the Quotient Monoid of Associated Elements
Informal description
For any element $a$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is primal if and only if $a$ is primal in $M$. That is, $\text{Associates.mk}\, a$ is primal if and only if for any $b, c \in M$ such that $a$ divides $b \cdot c$, there exist $a_1, a_2 \in M$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $a = a_1 \cdot a_2$.
Associates.decompositionMonoid_iff theorem
: DecompositionMonoid (Associates M) ↔ DecompositionMonoid M
Full source 
@[simp]
theorem decompositionMonoid_iff : DecompositionMonoidDecompositionMonoid (Associates M) ↔ DecompositionMonoid M := by
  simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]
Decomposition Monoid Property of Quotient $\text{Associates}\, M$
Informal description
The quotient monoid $\text{Associates}\, M$ is a decomposition monoid if and only if the original monoid $M$ is a decomposition monoid. In other words, every element in $\text{Associates}\, M$ is primal precisely when every element in $M$ is primal.
Associates.mk_isRelPrime_iff theorem
{a b : M} : IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
Full source 
@[simp]
theorem mk_isRelPrime_iff {a b : M} :
    IsRelPrimeIsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b := by
  simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]
Relatively Prime Elements in Quotient Monoid iff Relatively Prime in Original Monoid
Informal description
For any elements $a$ and $b$ in a monoid $M$, the equivalence classes of $a$ and $b$ in the quotient monoid $\text{Associates}\, M$ are relatively prime if and only if $a$ and $b$ are relatively prime in $M$. In other words, $\text{IsRelPrime}\, (\text{Associates.mk}\, a)\, (\text{Associates.mk}\, b) \leftrightarrow \text{IsRelPrime}\, a\, b$.
Associates.instZero instance
[Zero M] [Monoid M] : Zero (Associates M)
Full source 
instance [Zero M] [Monoid M] : Zero (Associates M) :=
  ⟨⟦0⟧⟩
Zero Element in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$ with a zero element, the quotient monoid $\text{Associates}\, M$ of associated elements also has a zero element, which is the equivalence class of $0 \in M$.
Associates.instTopOfZero instance
[Zero M] [Monoid M] : Top (Associates M)
Full source 
instance [Zero M] [Monoid M] : Top (Associates M) :=
  ⟨0⟩
Top Element in the Quotient Monoid of Associated Elements with Zero
Informal description
For any monoid $M$ with a zero element, the quotient monoid $\text{Associates}\, M$ of associated elements has a top element, which is the equivalence class of $0 \in M$.
Associates.mk_zero theorem
[Zero M] [Monoid M] : Associates.mk (0 : M) = 0
Full source 
@[simp] theorem mk_zero [Zero M] [Monoid M] : Associates.mk (0 : M) = 0 := rfl
Zero Element in Quotient Monoid of Associated Elements
Informal description
For any monoid $M$ with a zero element, the equivalence class of $0$ in the quotient monoid $\text{Associates}\, M$ is equal to the zero element of $\text{Associates}\, M$, i.e., $\text{Associates.mk}(0) = 0$.
Associates.mk_eq_zero theorem
{a : M} : Associates.mk a = 0 ↔ a = 0
Full source 
@[simp]
theorem mk_eq_zero {a : M} : Associates.mkAssociates.mk a = 0 ↔ a = 0 :=
  ⟨fun h => (associated_zero_iff_eq_zero a).1 <| Quotient.exact h, fun h => h.symm ▸ rfl⟩
Characterization of Zero in the Quotient Monoid of Associated Elements
Informal description
For any element $a$ in a monoid $M$ with zero, the equivalence class of $a$ in the quotient monoid of associated elements is equal to the zero class if and only if $a$ is equal to zero. In other words, $\text{Associates.mk}\, a = 0 \leftrightarrow a = 0$.
Associates.quot_out_zero theorem
: Quot.out (0 : Associates M) = 0
Full source 
@[simp]
theorem quot_out_zero : Quot.out (0 : Associates M) = 0 := by rw [← mk_eq_zero, quot_out]
Representative of Zero in Quotient Monoid is Zero
Informal description
For the zero element $0$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, the representative selected by $\text{Quot.out}$ is equal to $0$ in $M$.
Associates.mk_ne_zero theorem
{a : M} : Associates.mk a ≠ 0 ↔ a ≠ 0
Full source 
theorem mk_ne_zero {a : M} : Associates.mkAssociates.mk a ≠ 0Associates.mk a ≠ 0 ↔ a ≠ 0 :=
  not_congr mk_eq_zero
Nonzero Characterization in the Quotient Monoid of Associated Elements
Informal description
For any element $a$ in a monoid $M$ with zero, the equivalence class of $a$ in the quotient monoid of associated elements is nonzero if and only if $a$ itself is nonzero. In other words, $\text{Associates.mk}\, a \neq 0 \leftrightarrow a \neq 0$.
Associates.exists_non_zero_rep theorem
{a : Associates M} : a ≠ 0 → ∃ a0 : M, a0 ≠ 0 ∧ Associates.mk a0 = a
Full source 
theorem exists_non_zero_rep {a : Associates M} : a ≠ 0 → ∃ a0 : M, a0 ≠ 0 ∧ Associates.mk a0 = a :=
  Quotient.inductionOn a fun b nz => ⟨b, mt (congr_arg Quotient.mk'') nz, rfl⟩
Existence of Nonzero Representative in Associates Monoid
Informal description
For any nonzero element $a$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, there exists a nonzero representative $a_0 \in M$ such that the equivalence class of $a_0$ in $\text{Associates}\, M$ is equal to $a$. In other words, if $a \neq 0$ in $\text{Associates}\, M$, then there exists $a_0 \in M$ with $a_0 \neq 0$ and $\text{Associates.mk}\, a_0 = a$.
Associates.instCommMonoidWithZero instance
: CommMonoidWithZero (Associates M)
Full source 
instance instCommMonoidWithZero : CommMonoidWithZero (Associates M) where
    zero_mul := forall_associated.2 fun a ↦ by rw [← mk_zero, mk_mul_mk, zero_mul]
    mul_zero := forall_associated.2 fun a ↦ by rw [← mk_zero, mk_mul_mk, mul_zero]
Commutative Monoid with Zero Structure on the Quotient of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements is a commutative monoid with zero. The multiplication operation on $\text{Associates}\, M$ is commutative, has a multiplicative identity, and includes a zero element that is absorbing.
Associates.instOrderTop instance
: OrderTop (Associates M)
Full source 
instance instOrderTop : OrderTop (Associates M) where
  top := 0
  le_top := dvd_zero
Greatest Element in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements has a greatest element with respect to the divisibility preorder. This greatest element is the equivalence class of $0 \in M$ (if $M$ has a zero element), and it satisfies $a \leq 0$ for all $a \in \text{Associates}\, M$.
Associates.le_zero theorem
(a : Associates M) : a ≤ 0
Full source 
@[simp] protected theorem le_zero (a : Associates M) : a ≤ 0 := le_top
Every Element is Divisible by Zero in the Quotient of Associated Elements
Informal description
For any element $a$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$ with zero, we have $a \leq 0$ with respect to the divisibility preorder.
Associates.instBoundedOrder instance
: BoundedOrder (Associates M)
Full source 
instance instBoundedOrder : BoundedOrder (Associates M) where
Bounded Divisibility Preorder on the Quotient of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements is a bounded order with respect to the divisibility preorder. This means it has both a greatest element (the equivalence class of $0$) and a least element (the equivalence class of $1$).
Associates.instDecidableRelDvd instance
[DecidableRel ((· ∣ ·) : M → M → Prop)] : DecidableRel ((· ∣ ·) : Associates M → Associates M → Prop)
Full source 
instance [DecidableRel ((· ∣ ·) : M → M → Prop)] :
    DecidableRel ((· ∣ ·) : Associates M → Associates M → Prop) := fun a b =>
  Quotient.recOnSubsingleton₂ a b fun _ _ => decidable_of_iff' _ mk_dvd_mk
Decidability of Divisibility in the Quotient of Associated Elements
Informal description
For any monoid $M$ with a decidable divisibility relation on $M$, the divisibility relation on the quotient monoid $\text{Associates}\, M$ of associated elements is also decidable.
Associates.Prime.le_or_le theorem
{p : Associates M} (hp : Prime p) {a b : Associates M} (h : p ≤ a * b) : p ≤ a ∨ p ≤ b
Full source 
theorem Prime.le_or_le {p : Associates M} (hp : Prime p) {a b : Associates M} (h : p ≤ a * b) :
    p ≤ a ∨ p ≤ b :=
  hp.2.2 a b h
Prime Divisibility Property in Quotient Monoid of Associated Elements
Informal description
Let $M$ be a monoid and let $p$ be a prime element in the quotient monoid $\text{Associates}\, M$ of associated elements. For any elements $a, b \in \text{Associates}\, M$, if $p$ divides the product $a \cdot b$, then $p$ divides $a$ or $p$ divides $b$.
Associates.prime_mk theorem
{p : M} : Prime (Associates.mk p) ↔ Prime p
Full source 
@[simp]
theorem prime_mk {p : M} : PrimePrime (Associates.mk p) ↔ Prime p := by
  rw [Prime, _root_.Prime, forall_associated]
  simp only [forall_associated, mk_ne_zero, isUnit_mk, mk_mul_mk, mk_dvd_mk]
Prime Elements in the Quotient Monoid of Associated Elements
Informal description
For any element $p$ in a monoid $M$, the equivalence class of $p$ in the quotient monoid $\text{Associates}\, M$ is a prime element if and only if $p$ is a prime element in $M$.
Associates.irreducible_mk theorem
{a : M} : Irreducible (Associates.mk a) ↔ Irreducible a
Full source 
@[simp]
theorem irreducible_mk {a : M} : IrreducibleIrreducible (Associates.mk a) ↔ Irreducible a := by
  simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]
  apply Iff.rfl.and
  constructor
  · rintro h x y rfl
    exact h _ _ <| .refl _
  · rintro h x y ⟨u, rfl⟩
    simpa using h (mul_assoc _ _ _)
Irreducibility in the Quotient Monoid of Associated Elements
Informal description
For any element $a$ in a monoid $M$, the equivalence class of $a$ in the quotient monoid $\text{Associates}\, M$ is irreducible if and only if $a$ is irreducible in $M$.
Associates.mk_dvdNotUnit_mk_iff theorem
{a b : M} : DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
Full source 
@[simp]
theorem mk_dvdNotUnit_mk_iff {a b : M} :
    DvdNotUnitDvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b := by
  simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := b)]
  refine Iff.rfl.and ?_
  constructor
  · rintro ⟨x, hx, u, rfl⟩
    refine ⟨x * u, ?_, mul_assoc ..⟩
    simpa
  · rintro ⟨x, ⟨hx, rfl⟩⟩
    use x
Strict Divisibility in Quotient Monoid of Associated Elements Reflects Strict Divisibility in Original Monoid
Informal description
For any elements $a$ and $b$ in a monoid $M$, the equivalence class of $a$ strictly divides the equivalence class of $b$ in the quotient monoid $\text{Associates}\, M$ if and only if $a$ strictly divides $b$ in $M$. Here, strict divisibility means that $a$ is a non-zero divisor of $b$ and the quotient $b/a$ is not a unit in $M$.
Associates.dvdNotUnit_of_lt theorem
{a b : Associates M} (hlt : a < b) : DvdNotUnit a b
Full source 
theorem dvdNotUnit_of_lt {a b : Associates M} (hlt : a < b) : DvdNotUnit a b := by
  constructor
  · rintro rfl
    apply not_lt_of_le _ hlt
    apply dvd_zero
  rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
  refine ⟨x, ?_, rfl⟩
  contrapose! ndvd
  rcases ndvd with ⟨u, rfl⟩
  simp
Strict Order Implies Strict Divisibility in Quotient Monoid of Associated Elements
Informal description
For any elements $a$ and $b$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, if $a < b$ in the canonical preorder, then $a$ strictly divides $b$, i.e., $a$ is a non-zero divisor of $b$ and the quotient $b/a$ is not a unit in $\text{Associates}\, M$.
Associates.irreducible_iff_prime_iff theorem
: (∀ a : M, Irreducible a ↔ Prime a) ↔ ∀ a : Associates M, Irreducible a ↔ Prime a
Full source 
theorem irreducible_iff_prime_iff :
    (∀ a : M, Irreducible a ↔ Prime a) ↔ ∀ a : Associates M, Irreducible a ↔ Prime a := by
  simp_rw [forall_associated, irreducible_mk, prime_mk]
Equivalence of Irreducibility and Primality in Monoid and its Associated Quotient
Informal description
For any monoid $M$, the following are equivalent: 1. Every irreducible element in $M$ is prime. 2. Every irreducible element in the quotient monoid $\text{Associates}\, M$ is prime.
Associates.instPartialOrder instance
: PartialOrder (Associates M)
Full source 
instance instPartialOrder : PartialOrder (Associates M) where
  le_antisymm := mk_surjective.forall₂.2 fun _a _b hab hba => mk_eq_mk_iff_associated.2 <|
    associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba)
Partial Order on the Quotient of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements is equipped with a canonical partial order structure, where the relation $\leq$ is defined via the divisibility relation in $M$.
Associates.instCancelCommMonoidWithZero instance
: CancelCommMonoidWithZero (Associates M)
Full source 
instance instCancelCommMonoidWithZero : CancelCommMonoidWithZero (Associates M) :=
  { (by infer_instance : CommMonoidWithZero (Associates M)) with
    mul_left_cancel_of_ne_zero := by
      rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
      rcases Quotient.exact' h with ⟨u, hu⟩
      have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
      exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩ }
Cancelative Commutative Monoid with Zero Structure on the Quotient of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements is a cancelative commutative monoid with zero. This means that the multiplication operation on $\text{Associates}\, M$ is commutative, has a multiplicative identity, includes a zero element that is absorbing, and satisfies the cancellation property for non-zero elements.
associates_irreducible_iff_prime theorem
[DecompositionMonoid M] {p : Associates M} : Irreducible p ↔ Prime p
Full source 
theorem _root_.associates_irreducible_iff_prime [DecompositionMonoid M] {p : Associates M} :
    IrreducibleIrreducible p ↔ Prime p := irreducible_iff_prime
Irreducible Elements are Prime in the Quotient of a Decomposition Monoid
Informal description
Let $M$ be a decomposition monoid and let $p$ be an element of the quotient monoid $\text{Associates}\, M$ of associated elements. Then $p$ is irreducible if and only if $p$ is prime.
Associates.instNoZeroDivisors instance
: NoZeroDivisors (Associates M)
Full source 
instance : NoZeroDivisors (Associates M) := by infer_instance
No Zero Divisors in the Quotient Monoid of Associated Elements
Informal description
For any monoid $M$, the quotient monoid $\text{Associates}\, M$ of associated elements has no zero divisors. That is, for any elements $[x]$ and $[y]$ in $\text{Associates}\, M$, if $[x] \cdot [y] = [0]$, then either $[x] = [0]$ or $[y] = [0]$.
Associates.le_of_mul_le_mul_left theorem
(a b c : Associates M) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c
Full source 
theorem le_of_mul_le_mul_left (a b c : Associates M) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c
  | ⟨d, hd⟩ => ⟨d, mul_left_cancel₀ ha <| by rwa [← mul_assoc]⟩
Left Cancellation of Divisibility in the Quotient Monoid of Associated Elements
Informal description
For any elements $a, b, c$ in the quotient monoid $\text{Associates}\, M$ of associated elements of a monoid $M$, if $a \neq 0$ and $a \cdot b \leq a \cdot c$ in the divisibility preorder, then $b \leq c$.
Associates.one_or_eq_of_le_of_prime theorem
{p m : Associates M} (hp : Prime p) (hle : m ≤ p) : m = 1 ∨ m = p
Full source 
theorem one_or_eq_of_le_of_prime {p m : Associates M} (hp : Prime p) (hle : m ≤ p) :
    m = 1 ∨ m = p := by
  rcases mk_surjective p with ⟨p, rfl⟩
  rcases mk_surjective m with ⟨m, rfl⟩
  simpa [mk_eq_mk_iff_associated, Associated.comm, -Quotient.eq]
    using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)
Prime Divisibility Property in Quotient Monoid of Associated Elements
Informal description
Let $M$ be a monoid and let $p, m$ be elements in the quotient monoid $\text{Associates}\, M$ of associated elements. If $p$ is prime and $m$ divides $p$ (i.e., $m \leq p$ in the divisibility preorder), then either $m$ is the identity element $1$ or $m$ is equal to $p$.
Associates.dvdNotUnit_iff_lt theorem
{a b : Associates M} : DvdNotUnit a b ↔ a < b
Full source 
theorem dvdNotUnit_iff_lt {a b : Associates M} : DvdNotUnitDvdNotUnit a b ↔ a < b :=
  dvd_and_not_dvd_iff.symm
Equivalence of Strict Divisibility and Preorder in Quotient Monoid of Associated Elements
Informal description
For any elements $a, b$ in the quotient monoid $\text{Associates}\, M$ of associated elements, the strict divisibility relation $\text{DvdNotUnit}\, a\, b$ holds if and only if $a$ is strictly less than $b$ in the canonical preorder on $\text{Associates}\, M$.
Associates.le_one_iff theorem
{p : Associates M} : p ≤ 1 ↔ p = 1
Full source 
theorem le_one_iff {p : Associates M} : p ≤ 1 ↔ p = 1 := by rw [← Associates.bot_eq_one, le_bot_iff]
Characterization of Identity in Divisibility Preorder on Associated Elements: $p \leq 1 \leftrightarrow p = 1$
Informal description
For any element $p$ in the quotient monoid $\text{Associates}\, M$ of associated elements, the inequality $p \leq 1$ holds if and only if $p$ is equal to the multiplicative identity $1$.
dvdNotUnit_of_dvdNotUnit_associated theorem
[CommMonoidWithZero M] [Nontrivial M] {p q r : M} (h : DvdNotUnit p q) (h' : Associated q r) : DvdNotUnit p r
Full source 
theorem dvdNotUnit_of_dvdNotUnit_associated [CommMonoidWithZero M] [Nontrivial M] {p q r : M}
    (h : DvdNotUnit p q) (h' : Associated q r) : DvdNotUnit p r := by
  obtain ⟨u, rfl⟩ := Associated.symm h'
  obtain ⟨hp, x, hx⟩ := h
  refine ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩
  rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
Strict Divisibility Preserved Under Associated Elements in Commutative Monoid with Zero
Informal description
Let $M$ be a nontrivial commutative monoid with zero. For any elements $p, q, r \in M$, if $p$ strictly divides $q$ (i.e., $p \neq 0$ and there exists a non-unit $x$ such that $q = p \cdot x$) and $q$ is associated to $r$ (i.e., there exists a unit $u$ such that $q \cdot u = r$), then $p$ strictly divides $r$.
isUnit_of_associated_mul theorem
[CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p) (hp : p ≠ 0) : IsUnit b
Full source 
theorem isUnit_of_associated_mul [CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p)
    (hp : p ≠ 0) : IsUnit b := by
  obtain ⟨a, ha⟩ := h
  refine isUnit_of_mul_eq_one b a ((mul_right_inj' hp).mp ?_)
  rwa [← mul_assoc, mul_one]
Associated Product Implies Invertibility in Cancellative Monoid with Zero
Informal description
Let $M$ be a cancellative commutative monoid with zero. For any elements $p, b \in M$ with $p \neq 0$, if $p \cdot b$ is associated to $p$, then $b$ is a unit in $M$.
DvdNotUnit.not_associated theorem
[CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) : ¬Associated p q
Full source 
theorem DvdNotUnit.not_associated [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) :
    ¬Associated p q := by
  rintro ⟨a, rfl⟩
  obtain ⟨hp, x, hx, hx'⟩ := h
  rcases (mul_right_inj' hp).mp hx' with rfl
  exact hx a.isUnit
Strict Divisibility Implies Non-Associated Elements in Cancellative Monoids
Informal description
Let $M$ be a cancellative commutative monoid with zero. For any elements $p, q \in M$, if $p$ strictly divides $q$ (i.e., $p \neq 0$ and there exists a non-unit $x$ such that $q = p \cdot x$), then $p$ and $q$ are not associated (i.e., there is no unit $u$ such that $p \cdot u = q$).
dvd_prime_pow theorem
[CancelCommMonoidWithZero M] {p q : M} (hp : Prime p) (n : ℕ) : q ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i)
Full source 
theorem dvd_prime_pow [CancelCommMonoidWithZero M] {p q : M} (hp : Prime p) (n : ℕ) :
    q ∣ p ^ nq ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i) := by
  induction n generalizing q with
  | zero =>
    simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
  | succ n ih =>
    refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
    rw [pow_succ'] at h
    rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
    · rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
      rcases h with ⟨i, hi, hq⟩
      refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
      rw [pow_succ']
    · obtain ⟨i, hi, hq⟩ := ih.mp hno
      exact ⟨i, hi.trans n.le_succ, hq⟩
Divisibility of Prime Powers in Cancellative Monoids: $q \mid p^n \leftrightarrow \exists i \leq n, q \sim p^i$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any element $q \in M$ and natural number $n$, the element $q$ divides $p^n$ if and only if there exists an index $i$ with $0 \leq i \leq n$ such that $q$ is associated to $p^i$ (i.e., $q \sim p^i$).