Mathlib.Algebra.GCDMonoid.Basic

NormalizationMonoid structure

(α : Type*) [CancelCommMonoidWithZero α]

Full source

/-- Normalization monoid: multiplying with `normUnit` gives a normal form for associated
elements. -/
class NormalizationMonoid (α : Type*) [CancelCommMonoidWithZero α] where
  /-- `normUnit` assigns to each element of the monoid a unit of the monoid. -/
  normUnit : α → αˣ
  /-- The proposition that `normUnit` maps `0` to the identity. -/
  normUnit_zero : normUnit 0 = 1
  /-- The proposition that `normUnit` respects multiplication of non-zero elements. -/
  normUnit_mul : ∀ {a b}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
  /-- The proposition that `normUnit` maps units to their inverses. -/
  normUnit_coe_units : ∀ u : αˣ, normUnit u = u⁻¹

Normalization Monoid

Informal description

A normalization monoid is a structure on a commutative monoid with zero and cancellation (`CancelCommMonoidWithZero`) where each element has an associated unit `normUnit` such that multiplying by this unit yields a normalized form. The normalization function `normalize` is an idempotent monoid homomorphism that maps elements to their normalized forms.

normUnit_one theorem

: normUnit (1 : α) = 1

Full source

@[simp]
theorem normUnit_one : normUnit (1 : α) = 1 :=
  normUnit_coe_units 1

Normalization Unit of Identity is Identity

Informal description

In a normalization monoid $\alpha$, the normalization unit of the multiplicative identity element $1$ is itself $1$, i.e., $\text{normUnit}(1) = 1$.

normalize definition

: α →*₀ α

Full source

/-- Chooses an element of each associate class, by multiplying by `normUnit` -/
def normalize : α →*₀ α where
  toFun x := x * normUnit x
  map_zero' := by
    simp only [normUnit_zero]
    exact mul_one (0 : α)
  map_one' := by rw [normUnit_one, one_mul]; rfl
  map_mul' x y :=
    (by_cases fun hx : x = 0 => by rw [hx, zero_mul, zero_mul, zero_mul]) fun hx =>
      (by_cases fun hy : y = 0 => by rw [hy, mul_zero, zero_mul, mul_zero]) fun hy => by
        simp only [normUnit_mul hx hy, Units.val_mul]; simp only [mul_assoc, mul_left_comm y]

Normalization function for monoids

Informal description

The function `normalize` maps each element $x$ of a normalization monoid $\alpha$ to its normalized form $x \cdot \text{normUnit}(x)$, where $\text{normUnit}(x)$ is a unit such that multiplying by it yields a normalized representative of the associate class of $x$. The function is an idempotent monoid homomorphism that preserves the multiplicative structure.

associated_normalize theorem

(x : α) : Associated x (normalize x)

Full source

theorem associated_normalize (x : α) : Associated x (normalize x) :=
  ⟨_, rfl⟩

Association Between Element and Its Normalized Form

Informal description

For any element $x$ in a normalization monoid $\alpha$, $x$ is associated with its normalized form $\text{normalize}(x)$.

normalize_associated theorem

(x : α) : Associated (normalize x) x

Full source

theorem normalize_associated (x : α) : Associated (normalize x) x :=
  (associated_normalize _).symm

Normalized Form is Associated with Original Element

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalized form $\text{normalize}(x)$ is associated with $x$.

associated_normalize_iff theorem

{x y : α} : Associated x (normalize y) ↔ Associated x y

Full source

theorem associated_normalize_iff {x y : α} : AssociatedAssociated x (normalize y) ↔ Associated x y :=
  ⟨fun h => h.trans (normalize_associated y), fun h => h.trans (associated_normalize y)⟩

Equivalence of Association with Normalized Form: $x \sim \text{normalize}(y) \leftrightarrow x \sim y$

Informal description

For any two elements $x$ and $y$ in a normalization monoid $\alpha$, the element $x$ is associated with the normalized form of $y$ if and only if $x$ is associated with $y$ itself. In other words, $x \sim \text{normalize}(y) \leftrightarrow x \sim y$, where $\sim$ denotes the associated relation.

normalize_associated_iff theorem

{x y : α} : Associated (normalize x) y ↔ Associated x y

Full source

theorem normalize_associated_iff {x y : α} : AssociatedAssociated (normalize x) y ↔ Associated x y :=
  ⟨fun h => (associated_normalize _).trans h, fun h => (normalize_associated _).trans h⟩

Normalized Association Criterion: $\text{normalize}(x) \sim y \leftrightarrow x \sim y$

Informal description

For any elements $x$ and $y$ in a normalization monoid $\alpha$, the normalized form $\text{normalize}(x)$ is associated with $y$ if and only if $x$ is associated with $y$.

Associates.mk_normalize theorem

(x : α) : Associates.mk (normalize x) = Associates.mk x

Full source

theorem Associates.mk_normalize (x : α) : Associates.mk (normalize x) = Associates.mk x :=
  Associates.mk_eq_mk_iff_associated.2 (normalize_associated _)

Equivalence of Normalized Form and Original Element in Associates

Informal description

For any element $x$ in a normalization monoid $\alpha$, the equivalence class of the normalized form of $x$ under the associates relation is equal to the equivalence class of $x$ itself, i.e., $\text{Associates.mk}(\text{normalize}(x)) = \text{Associates.mk}(x)$.

normalize_apply theorem

(x : α) : normalize x = x * normUnit x

Full source

theorem normalize_apply (x : α) : normalize x = x * normUnit x :=
  rfl

Normalization Formula: $\text{normalize}(x) = x \cdot \text{normUnit}(x)$

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalized form of $x$ is given by $\text{normalize}(x) = x \cdot \text{normUnit}(x)$, where $\text{normUnit}(x)$ is the associated unit that normalizes $x$.

normalize_zero theorem

: normalize (0 : α) = 0

Full source

theorem normalize_zero : normalize (0 : α) = 0 :=
  normalize.map_zero

Normalization of Zero: $\text{normalize}(0) = 0$

Informal description

In a normalization monoid $\alpha$, the normalization function applied to the zero element $0$ yields $0$, i.e., $\text{normalize}(0) = 0$.

normalize_one theorem

: normalize (1 : α) = 1

Full source

theorem normalize_one : normalize (1 : α) = 1 :=
  normalize.map_one

Normalization of Identity: $\text{normalize}(1) = 1$

Informal description

In a normalization monoid $\alpha$, the normalization function applied to the multiplicative identity $1$ yields $1$, i.e., $\text{normalize}(1) = 1$.

normalize_coe_units theorem

(u : αˣ) : normalize (u : α) = 1

Full source

theorem normalize_coe_units (u : αˣ) : normalize (u : α) = 1 := by simp [normalize_apply]

Normalization of Units Yields Identity: $\text{normalize}(u) = 1$

Informal description

For any unit $u$ in the group of units $\alpha^\times$ of a normalization monoid $\alpha$, the normalization of $u$ (considered as an element of $\alpha$) is equal to the multiplicative identity, i.e., $\text{normalize}(u) = 1$.

normalize_eq_zero theorem

{x : α} : normalize x = 0 ↔ x = 0

Full source

theorem normalize_eq_zero {x : α} : normalizenormalize x = 0 ↔ x = 0 :=
  ⟨fun hx => (associated_zero_iff_eq_zero x).1 <| hx ▸ associated_normalize _, by
    rintro rfl; exact normalize_zero⟩

Normalization Yields Zero if and Only if Element is Zero

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalized form of $x$ is zero if and only if $x$ itself is zero, i.e., $\text{normalize}(x) = 0 \leftrightarrow x = 0$.

normalize_eq_one theorem

{x : α} : normalize x = 1 ↔ IsUnit x

Full source

theorem normalize_eq_one {x : α} : normalizenormalize x = 1 ↔ IsUnit x :=
  ⟨fun hx => isUnit_iff_exists_inv.2 ⟨_, hx⟩, fun ⟨u, hu⟩ => hu ▸ normalize_coe_units u⟩

Normalization Equals One iff Element is a Unit

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalized form of $x$ is equal to $1$ if and only if $x$ is a unit, i.e., $\text{normalize}(x) = 1 \leftrightarrow \text{IsUnit}(x)$.

normUnit_mul_normUnit theorem

(a : α) : normUnit (a * normUnit a) = 1

Full source

@[simp]
theorem normUnit_mul_normUnit (a : α) : normUnit (a * normUnit a) = 1 := by
  nontriviality α using Subsingleton.elim a 0
  obtain rfl | h := eq_or_ne a 0
  · rw [normUnit_zero, zero_mul, normUnit_zero]
  · rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]

Normalization Unit Property: $\text{normUnit}(a \cdot \text{normUnit}(a)) = 1$

Informal description

For any element $a$ in a normalization monoid $\alpha$, the normalization unit of the product $a \cdot \text{normUnit}(a)$ is equal to $1$.

normalize_idem theorem

(x : α) : normalize (normalize x) = normalize x

Full source

@[simp]
theorem normalize_idem (x : α) : normalize (normalize x) = normalize x := by simp [normalize_apply]

Idempotence of Normalization Function

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalization function is idempotent, i.e., $\text{normalize}(\text{normalize}(x)) = \text{normalize}(x)$.

normalize_eq_normalize theorem

{a b : α} (hab : a ∣ b) (hba : b ∣ a) : normalize a = normalize b

Full source

theorem normalize_eq_normalize {a b : α} (hab : a ∣ b) (hba : b ∣ a) :
    normalize a = normalize b := by
  nontriviality α
  rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩
  refine by_cases (by rintro rfl; simp only [zero_mul]) fun ha : a ≠ 0 => ?_
  suffices a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹ by
    simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]
  calc
    a * ↑(normUnit a) = a * ↑(normUnit a) * ↑u * ↑u⁻¹ := (Units.mul_inv_cancel_right _ _).symm
    _ = a * ↑u * ↑(normUnit a) * ↑u⁻¹ := by rw [mul_right_comm a]

Normalized Forms of Associated Elements Are Equal

Informal description

For any elements $a$ and $b$ in a normalization monoid $\alpha$, if $a$ divides $b$ and $b$ divides $a$, then their normalized forms are equal, i.e., $\text{normalize}(a) = \text{normalize}(b)$.

normalize_eq_normalize_iff theorem

{x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x

Full source

theorem normalize_eq_normalize_iff {x y : α} : normalizenormalize x = normalize y ↔ x ∣ y ∧ y ∣ x :=
  ⟨fun h => ⟨Units.dvd_mul_right.1 ⟨_, h.symm⟩, Units.dvd_mul_right.1 ⟨_, h⟩⟩, fun ⟨hxy, hyx⟩ =>
    normalize_eq_normalize hxy hyx⟩

Equality of Normalized Forms is Equivalent to Mutual Divisibility

Informal description

For any elements $x$ and $y$ in a normalization monoid $\alpha$, the normalized forms of $x$ and $y$ are equal if and only if $x$ divides $y$ and $y$ divides $x$, i.e., $\text{normalize}(x) = \text{normalize}(y) \leftrightarrow x \mid y \land y \mid x$.

dvd_antisymm_of_normalize_eq theorem

{a b : α} (ha : normalize a = a) (hb : normalize b = b) (hab : a ∣ b) (hba : b ∣ a) : a = b

Full source

theorem dvd_antisymm_of_normalize_eq {a b : α} (ha : normalize a = a) (hb : normalize b = b)
    (hab : a ∣ b) (hba : b ∣ a) : a = b :=
  ha ▸ hb ▸ normalize_eq_normalize hab hba

Antisymmetry of Divisibility for Normalized Elements

Informal description

For any elements $a$ and $b$ in a normalization monoid $\alpha$, if $a$ and $b$ are already in their normalized forms (i.e., $\text{normalize}(a) = a$ and $\text{normalize}(b) = b$) and they divide each other ($a \mid b$ and $b \mid a$), then $a = b$.

dvd_normalize_iff theorem

{a b : α} : a ∣ normalize b ↔ a ∣ b

Full source

@[simp]
theorem dvd_normalize_iff {a b : α} : a ∣ normalize ba ∣ normalize b ↔ a ∣ b :=
  Units.dvd_mul_right

Divisibility Condition for Normalized Elements

Informal description

For any elements $a$ and $b$ in a normalization monoid $\alpha$, the element $a$ divides the normalized form of $b$ if and only if $a$ divides $b$. In other words, $a \mid \text{normalize}(b) \leftrightarrow a \mid b$.

normalize_dvd_iff theorem

{a b : α} : normalize a ∣ b ↔ a ∣ b

Full source

@[simp]
theorem normalize_dvd_iff {a b : α} : normalizenormalize a ∣ bnormalize a ∣ b ↔ a ∣ b :=
  Units.mul_right_dvd

Normalized Divisor Equivalence

Informal description

For any elements $a$ and $b$ in a normalization monoid $\alpha$, the normalized form of $a$ divides $b$ if and only if $a$ divides $b$. In other words, $\text{normalize}(a) \mid b \leftrightarrow a \mid b$.

Associates.out definition

: Associates α → α

Full source

/-- Maps an element of `Associates` back to the normalized element of its associate class -/
protected def out : Associates α → α :=
  (Quotient.lift (normalize : α → α)) fun a _ ⟨_, hu⟩ =>
    hu ▸ normalize_eq_normalize ⟨_, rfl⟩ (Units.mul_right_dvd.2 <| dvd_refl a)

Normalized representative of an associate class

Informal description

The function maps an element of the `Associates` of a monoid $\alpha$ to the normalized representative of its associate class. Specifically, for any element $a$ in the monoid, the output of `Associates.out` applied to the equivalence class of $a$ is the normalized form of $a$.

Associates.out_mk theorem

(a : α) : (Associates.mk a).out = normalize a

Full source

@[simp]
theorem out_mk (a : α) : (Associates.mk a).out = normalize a :=
  rfl

Normalized Representative of Associate Class Equals Normalization

Informal description

For any element $a$ in a normalization monoid $\alpha$, the normalized representative of the associate class of $a$ is equal to the normalization of $a$, i.e., $\text{out}(\text{mk}(a)) = \text{normalize}(a)$.

Associates.out_one theorem

: (1 : Associates α).out = 1

Full source

@[simp]
theorem out_one : (1 : Associates α).out = 1 :=
  normalize_one

Normalized Representative of Identity in Associates Monoid

Informal description

In the associates monoid of $\alpha$, the normalized representative of the multiplicative identity $1$ is $1$ itself, i.e., $\text{out}(1) = 1$.

Associates.out_mul theorem

(a b : Associates α) : (a * b).out = a.out * b.out

Full source

theorem out_mul (a b : Associates α) : (a * b).out = a.out * b.out :=
  Quotient.inductionOn₂ a b fun _ _ => by
    simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]

Multiplicativity of Normalized Representatives in Associates Monoid

Informal description

For any elements $a$ and $b$ in the associates monoid of a normalization monoid $\alpha$, the normalized representative of the product $a * b$ is equal to the product of the normalized representatives of $a$ and $b$, i.e., $\text{out}(a * b) = \text{out}(a) * \text{out}(b)$.

Associates.dvd_out_iff theorem

(a : α) (b : Associates α) : a ∣ b.out ↔ Associates.mk a ≤ b

Full source

theorem dvd_out_iff (a : α) (b : Associates α) : a ∣ b.outa ∣ b.out ↔ Associates.mk a ≤ b :=
  Quotient.inductionOn b <| by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Divisibility Criterion for Normalized Representatives in Associates Monoid

Informal description

Let $\alpha$ be a normalization monoid. For any element $a \in \alpha$ and any element $b$ in the associates of $\alpha$, the element $a$ divides the normalized representative of $b$ if and only if the associate class of $a$ is less than or equal to $b$ in the divisibility order. In symbols: $$ a \mid b.\text{out} \leftrightarrow \text{Associates.mk}(a) \leq b $$

Associates.out_dvd_iff theorem

(a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associates.mk a

Full source

theorem out_dvd_iff (a : α) (b : Associates α) : b.out ∣ ab.out ∣ a ↔ b ≤ Associates.mk a :=
  Quotient.inductionOn b <| by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Divisibility Criterion for Normalized Representatives in Associates

Informal description

Let $\alpha$ be a normalization monoid. For any element $a \in \alpha$ and any element $b$ in the associates of $\alpha$, the normalized representative $b.\text{out}$ divides $a$ if and only if $b$ is less than or equal to the associate class of $a$ in the divisibility order.

Associates.out_top theorem

: (⊤ : Associates α).out = 0

Full source

@[simp]
theorem out_top : (⊤ : Associates α).out = 0 :=
  normalize_zero

Normalized Representative of Top Associate is Zero

Informal description

In the associates of a normalization monoid $\alpha$, the normalized representative of the top element (with respect to the divisibility order) is equal to $0$.

Associates.normalize_out theorem

(a : Associates α) : normalize a.out = a.out

Full source

@[simp]
theorem normalize_out (a : Associates α) : normalize a.out = a.out :=
  Quotient.inductionOn a normalize_idem

Normalization of Normalized Representative in Associates Monoid is Idempotent

Informal description

For any element $a$ in the associates of a normalization monoid $\alpha$, the normalization function applied to the normalized representative of $a$ returns the same representative, i.e., $\text{normalize}(a.\text{out}) = a.\text{out}$.

Associates.mk_out theorem

(a : Associates α) : Associates.mk a.out = a

Full source

@[simp]
theorem mk_out (a : Associates α) : Associates.mk a.out = a :=
  Quotient.inductionOn a mk_normalize

Equivalence Class of Normalized Representative in Associates Monoid

Informal description

For any element $a$ in the associates of a normalization monoid $\alpha$, the equivalence class of its normalized representative is equal to $a$ itself, i.e., $\text{Associates.mk}(a.\text{out}) = a$.

Associates.out_injective theorem

: Function.Injective (Associates.out : _ → α)

Full source

theorem out_injective : Function.Injective (Associates.out : _ → α) :=
  Function.LeftInverse.injective mk_out

Injectivity of the Normalized Representative Function in Associates Monoid

Informal description

The function `Associates.out`, which maps an element of the associates of a monoid $\alpha$ to its normalized representative, is injective. That is, for any two elements $a, b$ in the associates of $\alpha$, if $a.\text{out} = b.\text{out}$, then $a = b$.

GCDMonoid structure

(α : Type*) [CancelCommMonoidWithZero α]

Full source

/-- GCD monoid: a `CancelCommMonoidWithZero` with `gcd` (greatest common divisor) and
`lcm` (least common multiple) operations, determined up to a unit. The type class focuses on `gcd`
and we derive the corresponding `lcm` facts from `gcd`.
-/
class GCDMonoid (α : Type*) [CancelCommMonoidWithZero α] where
  /-- The greatest common divisor between two elements. -/
  gcd : α → α → α
  /-- The least common multiple between two elements. -/
  lcm : α → α → α
  /-- The GCD is a divisor of the first element. -/
  gcd_dvd_left : ∀ a b, gcd a b ∣ a
  /-- The GCD is a divisor of the second element. -/
  gcd_dvd_right : ∀ a b, gcd a b ∣ b
  /-- Any common divisor of both elements is a divisor of the GCD. -/
  dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b
  /-- The product of two elements is `Associated` with the product of their GCD and LCM. -/
  gcd_mul_lcm : ∀ a b, Associated (gcd a b * lcm a b) (a * b)
  /-- `0` is left-absorbing. -/
  lcm_zero_left : ∀ a, lcm 0 a = 0
  /-- `0` is right-absorbing. -/
  lcm_zero_right : ∀ a, lcm a 0 = 0

GCD Monoid

Informal description

A GCD monoid is a cancellative commutative monoid with zero, equipped with operations `gcd` (greatest common divisor) and `lcm` (least common multiple) that are determined up to a unit. The structure focuses primarily on the `gcd` operation, from which properties of `lcm` can be derived.

NormalizedGCDMonoid structure

(α : Type*) [CancelCommMonoidWithZero α] extends NormalizationMonoid α,
  GCDMonoid α

Full source

/-- Normalized GCD monoid: a `CancelCommMonoidWithZero` with normalization and `gcd`
(greatest common divisor) and `lcm` (least common multiple) operations. In this setting `gcd` and
`lcm` form a bounded lattice on the associated elements where `gcd` is the infimum, `lcm` is the
supremum, `1` is bottom, and `0` is top. The type class focuses on `gcd` and we derive the
corresponding `lcm` facts from `gcd`.
-/
class NormalizedGCDMonoid (α : Type*) [CancelCommMonoidWithZero α] extends NormalizationMonoid α,
  GCDMonoid α where
  /-- The GCD is normalized to itself. -/
  normalize_gcd : ∀ a b, normalize (gcd a b) = gcd a b
  /-- The LCM is normalized to itself. -/
  normalize_lcm : ∀ a b, normalize (lcm a b) = lcm a b

Normalized GCD Monoid

Informal description

A `NormalizedGCDMonoid` is a structure extending a `CancelCommMonoidWithZero` with a normalization function and greatest common divisor (`gcd`) and least common multiple (`lcm`) operations. In this setting, `gcd` and `lcm` form a bounded lattice on the associated elements where `gcd` is the infimum, `lcm` is the supremum, `1` is the bottom element, and `0` is the top element. The structure focuses on `gcd`, and the corresponding properties of `lcm` are derived from `gcd`.

instNonemptyNormalizationMonoid instance

[NormalizationMonoid α] : Nonempty (NormalizationMonoid α)

Full source

instance [NormalizationMonoid α] : Nonempty (NormalizationMonoid α) := ⟨‹_›⟩

Nonempty Type of Normalization Monoid Structures

Informal description

For any normalization monoid $\alpha$, the type of normalization monoid structures on $\alpha$ is nonempty.

instNonemptyGCDMonoid instance

[GCDMonoid α] : Nonempty (GCDMonoid α)

Full source

instance [GCDMonoid α] : Nonempty (GCDMonoid α) := ⟨‹_›⟩

Nonempty GCD Monoid Structure

Informal description

For any type $\alpha$ that is a GCD monoid, there exists a nonempty instance of the GCD monoid structure on $\alpha$.

instNonemptyNormalizedGCDMonoid instance

[NormalizedGCDMonoid α] : Nonempty (NormalizedGCDMonoid α)

Full source

instance [NormalizedGCDMonoid α] : Nonempty (NormalizedGCDMonoid α) := ⟨‹_›⟩

Nonempty Normalized GCD Monoid Structures

Informal description

For any type $\alpha$ with a normalized GCD monoid structure, the type of normalized GCD monoid structures on $\alpha$ is nonempty.

instNonemptyNormalizationMonoidOfNormalizedGCDMonoid instance

[h : Nonempty (NormalizedGCDMonoid α)] : Nonempty (NormalizationMonoid α)

Full source

instance [h : Nonempty (NormalizedGCDMonoid α)] : Nonempty (NormalizationMonoid α) :=
  h.elim fun _ ↦ inferInstance

Nonempty Normalization Monoid from Normalized GCD Monoid

Informal description

For any type $\alpha$ with a nonempty normalized GCD monoid structure, there exists a nonempty normalization monoid structure on $\alpha$.

instNonemptyGCDMonoidOfNormalizedGCDMonoid instance

[h : Nonempty (NormalizedGCDMonoid α)] : Nonempty (GCDMonoid α)

Full source

instance [h : Nonempty (NormalizedGCDMonoid α)] : Nonempty (GCDMonoid α) :=
  h.elim fun _ ↦ inferInstance

Nonempty GCD Monoid Structure from Normalized GCD Monoid

Informal description

For any type $\alpha$ with a nonempty normalized GCD monoid structure, there exists a nonempty GCD monoid structure on $\alpha$.

gcd_isUnit_iff_isRelPrime theorem

[GCDMonoid α] {a b : α} : IsUnit (gcd a b) ↔ IsRelPrime a b

Full source

theorem gcd_isUnit_iff_isRelPrime [GCDMonoid α] {a b : α} :
    IsUnitIsUnit (gcd a b) ↔ IsRelPrime a b :=
  ⟨fun h _ ha hb ↦ isUnit_of_dvd_unit (dvd_gcd ha hb) h, (· (gcd_dvd_left a b) (gcd_dvd_right a b))⟩

Characterization of Relatively Prime Elements via GCD in a GCD Monoid

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(a, b)$ is a unit if and only if $a$ and $b$ are relatively prime.

normalize_gcd theorem

[NormalizedGCDMonoid α] : ∀ a b : α, normalize (gcd a b) = gcd a b

Full source

@[simp]
theorem normalize_gcd [NormalizedGCDMonoid α] : ∀ a b : α, normalize (gcd a b) = gcd a b :=
  NormalizedGCDMonoid.normalize_gcd

Normalization of GCD: $\mathrm{normalize}(\gcd(a, b)) = \gcd(a, b)$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the normalized form of $\gcd(a, b)$ is equal to $\gcd(a, b)$ itself. In other words, the greatest common divisor is already in its normalized form.

gcd_mul_lcm theorem

[GCDMonoid α] : ∀ a b : α, Associated (gcd a b * lcm a b) (a * b)

Full source

theorem gcd_mul_lcm [GCDMonoid α] : ∀ a b : α, Associated (gcd a b * lcm a b) (a * b) :=
  GCDMonoid.gcd_mul_lcm

GCD-LCM Product Relation: $\gcd(a, b) \cdot \mathrm{lcm}(a, b) \sim a \cdot b$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the product of the greatest common divisor $\gcd(a, b)$ and the least common multiple $\mathrm{lcm}(a, b)$ is associated with the product $a \cdot b$. In other words, there exists a unit $u$ such that $\gcd(a, b) \cdot \mathrm{lcm}(a, b) = u \cdot (a \cdot b)$.

dvd_gcd_iff theorem

[GCDMonoid α] (a b c : α) : a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c

Full source

theorem dvd_gcd_iff [GCDMonoid α] (a b c : α) : a ∣ gcd b ca ∣ gcd b c ↔ a ∣ b ∧ a ∣ c :=
  Iff.intro (fun h => ⟨h.trans (gcd_dvd_left _ _), h.trans (gcd_dvd_right _ _)⟩) fun ⟨hab, hac⟩ =>
    dvd_gcd hab hac

Divisibility Characterization of GCD: $a \mid \gcd(b, c) \leftrightarrow a \mid b \land a \mid c$

Informal description

Let $α$ be a GCD monoid. For any elements $a, b, c \in α$, the element $a$ divides the greatest common divisor $\gcd(b, c)$ if and only if $a$ divides both $b$ and $c$.

gcd_comm theorem

[NormalizedGCDMonoid α] (a b : α) : gcd a b = gcd b a

Full source

theorem gcd_comm [NormalizedGCDMonoid α] (a b : α) : gcd a b = gcd b a :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

Commutativity of GCD: $\gcd(a, b) = \gcd(b, a)$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the greatest common divisor $\gcd(a, b)$ is equal to $\gcd(b, a)$.

gcd_comm' theorem

[GCDMonoid α] (a b : α) : Associated (gcd a b) (gcd b a)

Full source

theorem gcd_comm' [GCDMonoid α] (a b : α) : Associated (gcd a b) (gcd b a) :=
  associated_of_dvd_dvd (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

Commutativity of GCD up to Units in a GCD Monoid

Informal description

Let $α$ be a GCD monoid. For any elements $a, b \in α$, the greatest common divisor $\gcd(a, b)$ is associated to $\gcd(b, a)$.

gcd_assoc theorem

[NormalizedGCDMonoid α] (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k)

Full source

theorem gcd_assoc [NormalizedGCDMonoid α] (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
      (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
    (dvd_gcd
      (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
      ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))

Associativity of GCD: $\gcd(\gcd(m, n), k) = \gcd(m, \gcd(n, k))$

Informal description

For any elements $m$, $n$, and $k$ in a normalized GCD monoid $\alpha$, the greatest common divisor satisfies the associativity property: $\gcd(\gcd(m, n), k) = \gcd(m, \gcd(n, k))$.

gcd_assoc' theorem

[GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (gcd m (gcd n k))

Full source

theorem gcd_assoc' [GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (gcd m (gcd n k)) :=
  associated_of_dvd_dvd
    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
      (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
    (dvd_gcd
      (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
      ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))

Associativity of GCD up to Units in a GCD Monoid

Informal description

Let $α$ be a GCD monoid. For any elements $m, n, k \in α$, the greatest common divisor $\gcd(\gcd(m, n), k)$ is associated to $\gcd(m, \gcd(n, k))$.

instCommutativeGcd instance

[NormalizedGCDMonoid α] : Std.Commutative (α := α) gcd

Full source

instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) gcd where
  comm := gcd_comm

Commutativity of GCD in Normalized GCD Monoids

Informal description

For any normalized GCD monoid $\alpha$, the greatest common divisor operation $\gcd$ is commutative.

instAssociativeGcd instance

[NormalizedGCDMonoid α] : Std.Associative (α := α) gcd

Full source

instance [NormalizedGCDMonoid α] : Std.Associative (α := α) gcd where
  assoc := gcd_assoc

Associativity of GCD in Normalized GCD Monoids

Informal description

For any normalized GCD monoid $\alpha$, the greatest common divisor operation $\gcd$ is associative.

gcd_eq_normalize theorem

[NormalizedGCDMonoid α] {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) : gcd a b = normalize c

Full source

theorem gcd_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : gcdgcd a b ∣ c)
    (hcab : c ∣ gcd a b) : gcd a b = normalize c :=
  normalize_gcd a b ▸ normalize_eq_normalize habc hcab

GCD Equals Normalization of Associated Element

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$ such that $\gcd(a, b)$ divides $c$ and $c$ divides $\gcd(a, b)$, we have $\gcd(a, b) = \mathrm{normalize}(c)$.

gcd_zero_left theorem

[NormalizedGCDMonoid α] (a : α) : gcd 0 a = normalize a

Full source

@[simp]
theorem gcd_zero_left [NormalizedGCDMonoid α] (a : α) : gcd 0 a = normalize a :=
  gcd_eq_normalize (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))

GCD with Zero Left: $\gcd(0, a) = \mathrm{normalize}(a)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$, the greatest common divisor of $0$ and $a$ equals the normalization of $a$, i.e., $\gcd(0, a) = \mathrm{normalize}(a)$.

gcd_zero_left' theorem

[GCDMonoid α] (a : α) : Associated (gcd 0 a) a

Full source

theorem gcd_zero_left' [GCDMonoid α] (a : α) : Associated (gcd 0 a) a :=
  associated_of_dvd_dvd (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))

GCD with Zero Left: $\gcd(0, a) \sim a$

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(0, a)$ is associated with $a$.

gcd_zero_right theorem

[NormalizedGCDMonoid α] (a : α) : gcd a 0 = normalize a

Full source

@[simp]
theorem gcd_zero_right [NormalizedGCDMonoid α] (a : α) : gcd a 0 = normalize a :=
  gcd_eq_normalize (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))

GCD with Zero Right: $\gcd(a, 0) = \mathrm{normalize}(a)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$, the greatest common divisor of $a$ and $0$ equals the normalization of $a$, i.e., $\gcd(a, 0) = \mathrm{normalize}(a)$.

gcd_zero_right' theorem

[GCDMonoid α] (a : α) : Associated (gcd a 0) a

Full source

theorem gcd_zero_right' [GCDMonoid α] (a : α) : Associated (gcd a 0) a :=
  associated_of_dvd_dvd (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))

GCD with Zero Right: $\gcd(a, 0) \sim a$

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(a, 0)$ is associated with $a$.

gcd_eq_zero_iff theorem

[GCDMonoid α] (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0

Full source

@[simp]
theorem gcd_eq_zero_iff [GCDMonoid α] (a b : α) : gcdgcd a b = 0 ↔ a = 0 ∧ b = 0 :=
  Iff.intro
    (fun h => by
      let ⟨ca, ha⟩ := gcd_dvd_left a b
      let ⟨cb, hb⟩ := gcd_dvd_right a b
      rw [h, zero_mul] at ha hb
      exact ⟨ha, hb⟩)
    fun ⟨ha, hb⟩ => by
    rw [ha, hb, ← zero_dvd_iff]
    apply dvd_gcd <;> rfl

GCD Zero Criterion: $\gcd(a, b) = 0 \leftrightarrow a = 0 \land b = 0$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(a, b)$ is zero if and only if both $a$ and $b$ are zero.

gcd_ne_zero_of_left theorem

[GCDMonoid α] {a b : α} (ha : a ≠ 0) : gcd a b ≠ 0

Full source

theorem gcd_ne_zero_of_left [GCDMonoid α] {a b : α} (ha : a ≠ 0) : gcdgcd a b ≠ 0 := by
  simp_all

Nonzero Divisor Implies Nonzero GCD (Left Case)

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, if $a \neq 0$, then the greatest common divisor $\gcd(a, b)$ is not zero.

gcd_ne_zero_of_right theorem

[GCDMonoid α] {a b : α} (hb : b ≠ 0) : gcd a b ≠ 0

Full source

theorem gcd_ne_zero_of_right [GCDMonoid α] {a b : α} (hb : b ≠ 0) : gcdgcd a b ≠ 0 := by
  simp_all

Nonzero Divisor Implies Nonzero GCD (Right Case)

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, if $b \neq 0$, then the greatest common divisor $\gcd(a, b)$ is not zero.

gcd_one_left theorem

[NormalizedGCDMonoid α] (a : α) : gcd 1 a = 1

Full source

@[simp]
theorem gcd_one_left [NormalizedGCDMonoid α] (a : α) : gcd 1 a = 1 :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_left _ _) (one_dvd _)

GCD Identity: $\gcd(1, a) = 1$ in Normalized GCD Monoids

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the greatest common divisor of $1$ and $a$ is $1$, i.e., $\gcd(1, a) = 1$.

isUnit_gcd_one_left theorem

[GCDMonoid α] (a : α) : IsUnit (gcd 1 a)

Full source

@[simp]
theorem isUnit_gcd_one_left [GCDMonoid α] (a : α) : IsUnit (gcd 1 a) :=
  isUnit_of_dvd_one (gcd_dvd_left _ _)

GCD of One and Any Element is a Unit

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(1, a)$ is a unit.

gcd_one_left' theorem

[GCDMonoid α] (a : α) : Associated (gcd 1 a) 1

Full source

theorem gcd_one_left' [GCDMonoid α] (a : α) : Associated (gcd 1 a) 1 := by simp

GCD of One and Any Element is Associated with One

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(1, a)$ is associated with $1$.

gcd_one_right theorem

[NormalizedGCDMonoid α] (a : α) : gcd a 1 = 1

Full source

@[simp]
theorem gcd_one_right [NormalizedGCDMonoid α] (a : α) : gcd a 1 = 1 :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)

$\gcd(a, 1) = 1$ in a normalized GCD monoid

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the greatest common divisor of $a$ and $1$ is equal to $1$, i.e., $\gcd(a, 1) = 1$.

isUnit_gcd_one_right theorem

[GCDMonoid α] (a : α) : IsUnit (gcd a 1)

Full source

@[simp]
theorem isUnit_gcd_one_right [GCDMonoid α] (a : α) : IsUnit (gcd a 1) :=
  isUnit_of_dvd_one (gcd_dvd_right _ _)

Greatest Common Divisor with One is a Unit in GCD Monoid

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(a, 1)$ is a unit.

gcd_one_right' theorem

[GCDMonoid α] (a : α) : Associated (gcd a 1) 1

Full source

theorem gcd_one_right' [GCDMonoid α] (a : α) : Associated (gcd a 1) 1 := by simp

GCD with One is Associated to One

Informal description

For any element $a$ in a GCD monoid $\alpha$, the greatest common divisor $\gcd(a, 1)$ is associated with $1$.

gcd_dvd_gcd theorem

[GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d

Full source

theorem gcd_dvd_gcd [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : gcdgcd a c ∣ gcd b d :=
  dvd_gcd ((gcd_dvd_left _ _).trans hab) ((gcd_dvd_right _ _).trans hcd)

GCD Divisibility Preservation: $\gcd(a, c) \mid \gcd(b, d)$ under divisibility conditions

Informal description

Let $a, b, c, d$ be elements of a GCD monoid $\alpha$. If $a$ divides $b$ and $c$ divides $d$, then the greatest common divisor of $a$ and $c$ divides the greatest common divisor of $b$ and $d$, i.e., $\gcd(a, c) \mid \gcd(b, d)$.

Associated.gcd theorem

 [GCDMonoid α] {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) : Associated (gcd a₁ b₁) (gcd a₂ b₂)

Full source

protected theorem Associated.gcd [GCDMonoid α]
    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
    Associated (gcd a₁ b₁) (gcd a₂ b₂) :=
  associated_of_dvd_dvd (gcd_dvd_gcd ha.dvd hb.dvd) (gcd_dvd_gcd ha.dvd' hb.dvd')

GCD Preservation under Associated Elements

Informal description

Let $\alpha$ be a GCD monoid, and let $a_1, a_2, b_1, b_2$ be elements of $\alpha$ such that $a_1$ is associated to $a_2$ and $b_1$ is associated to $b_2$. Then the greatest common divisor $\gcd(a_1, b_1)$ is associated to $\gcd(a_2, b_2)$.

gcd_same theorem

[NormalizedGCDMonoid α] (a : α) : gcd a a = normalize a

Full source

@[simp]
theorem gcd_same [NormalizedGCDMonoid α] (a : α) : gcd a a = normalize a :=
  gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))

GCD of an Element with Itself Equals Its Normalization

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the greatest common divisor of $a$ with itself equals the normalization of $a$, i.e., $\gcd(a, a) = \mathrm{normalize}(a)$.

gcd_mul_left theorem

[NormalizedGCDMonoid α] (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c

Full source

@[simp]
theorem gcd_mul_left [NormalizedGCDMonoid α] (a b c : α) :
    gcd (a * b) (a * c) = normalize a * gcd b c :=
  (by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]))
    fun ha : a ≠ 0 =>
    suffices gcd (a * b) (a * c) = normalize (a * gcd b c) by simpa
    let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
    gcd_eq_normalize
      (eq.symm ▸ mul_dvd_mul_left a
        (show d ∣ gcd b c from
          dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
            ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)))
      (dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _))

GCD Left Multiplication Identity: $\gcd(ab, ac) = \mathrm{normalize}(a) \cdot \gcd(b, c)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$, the greatest common divisor of $a \cdot b$ and $a \cdot c$ equals the normalization of $a$ multiplied by the greatest common divisor of $b$ and $c$, i.e., \[ \gcd(a \cdot b, a \cdot c) = \mathrm{normalize}(a) \cdot \gcd(b, c). \]

gcd_mul_left' theorem

[GCDMonoid α] (a b c : α) : Associated (gcd (a * b) (a * c)) (a * gcd b c)

Full source

theorem gcd_mul_left' [GCDMonoid α] (a b c : α) :
    Associated (gcd (a * b) (a * c)) (a * gcd b c) := by
  obtain rfl | ha := eq_or_ne a 0
  · simp only [zero_mul, gcd_zero_left']
  obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
  apply associated_of_dvd_dvd
  · rw [eq]
    apply mul_dvd_mul_left
    exact
      dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
        ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)
  · exact dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)

Left Multiplication Property of GCD in a GCD Monoid

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b, c \in \alpha$, the greatest common divisor of $a \cdot b$ and $a \cdot c$ is associated with $a$ multiplied by the greatest common divisor of $b$ and $c$, i.e., $\gcd(a \cdot b, a \cdot c) \sim a \cdot \gcd(b, c)$.

gcd_mul_right theorem

[NormalizedGCDMonoid α] (a b c : α) : gcd (b * a) (c * a) = gcd b c * normalize a

Full source

@[simp]
theorem gcd_mul_right [NormalizedGCDMonoid α] (a b c : α) :
    gcd (b * a) (c * a) = gcd b c * normalize a := by simp only [mul_comm, gcd_mul_left]

GCD Right Multiplication Identity: $\gcd(ba, ca) = \gcd(b, c) \cdot \mathrm{normalize}(a)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$, the greatest common divisor of $b \cdot a$ and $c \cdot a$ equals the greatest common divisor of $b$ and $c$ multiplied by the normalization of $a$, i.e., \[ \gcd(b \cdot a, c \cdot a) = \gcd(b, c) \cdot \mathrm{normalize}(a). \]

gcd_mul_right' theorem

[GCDMonoid α] (a b c : α) : Associated (gcd (b * a) (c * a)) (gcd b c * a)

Full source

@[simp]
theorem gcd_mul_right' [GCDMonoid α] (a b c : α) :
    Associated (gcd (b * a) (c * a)) (gcd b c * a) := by
  simp only [mul_comm, gcd_mul_left']

Right Multiplication Property of GCD in a GCD Monoid

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b, c \in \alpha$, the greatest common divisor of $b \cdot a$ and $c \cdot a$ is associated with the greatest common divisor of $b$ and $c$ multiplied by $a$, i.e., $\gcd(b \cdot a, c \cdot a) \sim \gcd(b, c) \cdot a$.

gcd_eq_left_iff theorem

[NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b

Full source

theorem gcd_eq_left_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) :
    gcdgcd a b = a ↔ a ∣ b :=
  (Iff.intro fun eq => eq ▸ gcd_dvd_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab)

GCD Equals Left Element if and only if Left Element Divides Right Element

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b \in \alpha$ where $a$ is already normalized (i.e., $\text{normalize}(a) = a$), the greatest common divisor $\gcd(a, b)$ equals $a$ if and only if $a$ divides $b$.

gcd_eq_right_iff theorem

[NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) : gcd a b = b ↔ b ∣ a

Full source

theorem gcd_eq_right_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) :
    gcdgcd a b = b ↔ b ∣ a := by simpa only [gcd_comm a b] using gcd_eq_left_iff b a h

GCD Equals Right Element if and only if Right Element Divides Left Element

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b \in \alpha$ where $b$ is already normalized (i.e., $\text{normalize}(b) = b$), the greatest common divisor $\gcd(a, b)$ equals $b$ if and only if $b$ divides $a$.

gcd_dvd_gcd_mul_left theorem

[GCDMonoid α] (m n k : α) : gcd m n ∣ gcd (k * m) n

Full source

theorem gcd_dvd_gcd_mul_left [GCDMonoid α] (m n k : α) : gcdgcd m n ∣ gcd (k * m) n :=
  gcd_dvd_gcd (dvd_mul_left _ _) dvd_rfl

GCD Divisibility Under Left Multiplication: $\gcd(m, n) \mid \gcd(k \cdot m, n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $k \cdot m$ and $n$.

gcd_dvd_gcd_mul_right theorem

[GCDMonoid α] (m n k : α) : gcd m n ∣ gcd (m * k) n

Full source

theorem gcd_dvd_gcd_mul_right [GCDMonoid α] (m n k : α) : gcdgcd m n ∣ gcd (m * k) n :=
  gcd_dvd_gcd (dvd_mul_right _ _) dvd_rfl

GCD Divisibility Under Right Multiplication: $\gcd(m, n) \mid \gcd(m \cdot k, n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m \cdot k$ and $n$, i.e., $\gcd(m, n) \mid \gcd(m \cdot k, n)$.

gcd_dvd_gcd_mul_left_right theorem

[GCDMonoid α] (m n k : α) : gcd m n ∣ gcd m (k * n)

Full source

theorem gcd_dvd_gcd_mul_left_right [GCDMonoid α] (m n k : α) : gcdgcd m n ∣ gcd m (k * n) :=
  gcd_dvd_gcd dvd_rfl (dvd_mul_left _ _)

GCD Divisibility Under Right Multiplication: $\gcd(m, n) \mid \gcd(m, k \cdot n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m$ and $k \cdot n$.

gcd_dvd_gcd_mul_right_right theorem

[GCDMonoid α] (m n k : α) : gcd m n ∣ gcd m (n * k)

Full source

theorem gcd_dvd_gcd_mul_right_right [GCDMonoid α] (m n k : α) : gcdgcd m n ∣ gcd m (n * k) :=
  gcd_dvd_gcd dvd_rfl (dvd_mul_right _ _)

GCD Divisibility Under Right Multiplication: $\gcd(m, n) \mid \gcd(m, n \cdot k)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m$ and $n \cdot k$.

Associated.gcd_eq_left theorem

[NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : gcd m k = gcd n k

Full source

theorem Associated.gcd_eq_left [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) :
    gcd m k = gcd n k :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (gcd_dvd_gcd h.dvd dvd_rfl)
    (gcd_dvd_gcd h.symm.dvd dvd_rfl)

GCD Equality for Associated Elements: $\gcd(m, k) = \gcd(n, k)$ when $m$ and $n$ are associated

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $m, n \in \alpha$ that are associated (i.e., $m$ and $n$ differ by a unit), and for any element $k \in \alpha$, the greatest common divisor of $m$ and $k$ equals the greatest common divisor of $n$ and $k$, i.e., $\gcd(m, k) = \gcd(n, k)$.

Associated.gcd_eq_right theorem

[NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : gcd k m = gcd k n

Full source

theorem Associated.gcd_eq_right [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) :
    gcd k m = gcd k n :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (gcd_dvd_gcd dvd_rfl h.dvd)
    (gcd_dvd_gcd dvd_rfl h.symm.dvd)

Right GCD Equality for Associated Elements: $\gcd(k, m) = \gcd(k, n)$ when $m \sim n$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $m, n, k \in \alpha$ such that $m$ and $n$ are associated (i.e., $m = u \cdot n$ for some unit $u$), the greatest common divisor of $k$ and $m$ is equal to the greatest common divisor of $k$ and $n$, i.e., $\gcd(k, m) = \gcd(k, n)$.

dvd_gcd_mul_of_dvd_mul theorem

[GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ gcd k m * n

Full source

theorem dvd_gcd_mul_of_dvd_mul [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ gcd k m * n :=
  (dvd_gcd (dvd_mul_right _ n) H).trans (gcd_mul_right' n k m).dvd

Divisibility Property of GCD in a GCD Monoid

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, if $k$ divides the product $m \cdot n$, then $k$ divides the product of $\gcd(k, m)$ and $n$, i.e., $k \mid \gcd(k, m) \cdot n$.

dvd_gcd_mul_iff_dvd_mul theorem

[GCDMonoid α] {m n k : α} : k ∣ gcd k m * n ↔ k ∣ m * n

Full source

theorem dvd_gcd_mul_iff_dvd_mul [GCDMonoid α] {m n k : α} : k ∣ gcd k m * nk ∣ gcd k m * n ↔ k ∣ m * n :=
  ⟨fun h => h.trans (mul_dvd_mul (gcd_dvd_right k m) dvd_rfl), dvd_gcd_mul_of_dvd_mul⟩

Divisibility Criterion via GCD: $k \mid \gcd(k, m) \cdot n \leftrightarrow k \mid m \cdot n$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the element $k$ divides the product $\gcd(k, m) \cdot n$ if and only if $k$ divides the product $m \cdot n$.

dvd_mul_gcd_of_dvd_mul theorem

[GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ m * gcd k n

Full source

theorem dvd_mul_gcd_of_dvd_mul [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ m * gcd k n := by
  rw [mul_comm] at H ⊢
  exact dvd_gcd_mul_of_dvd_mul H

Divisibility Property of GCD in a GCD Monoid (Right Version)

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, if $k$ divides the product $m \cdot n$, then $k$ divides the product of $m$ and $\gcd(k, n)$, i.e., $k \mid m \cdot \gcd(k, n)$.

dvd_mul_gcd_iff_dvd_mul theorem

[GCDMonoid α] {m n k : α} : k ∣ m * gcd k n ↔ k ∣ m * n

Full source

theorem dvd_mul_gcd_iff_dvd_mul [GCDMonoid α] {m n k : α} : k ∣ m * gcd k nk ∣ m * gcd k n ↔ k ∣ m * n :=
  ⟨fun h => h.trans (mul_dvd_mul dvd_rfl (gcd_dvd_right k n)), dvd_mul_gcd_of_dvd_mul⟩

Divisibility Criterion via GCD: $k \mid m \cdot \gcd(k, n) \leftrightarrow k \mid m \cdot n$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the element $k$ divides the product $m \cdot \gcd(k, n)$ if and only if $k$ divides the product $m \cdot n$.

instDecompositionMonoidOfNonemptyGCDMonoid instance

[h : Nonempty (GCDMonoid α)] : DecompositionMonoid α

Full source

/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.

Note: In general, this representation is highly non-unique.

See `Nat.dvdProdDvdOfDvdProd` for a constructive version on `ℕ`. -/
instance [h : Nonempty (GCDMonoid α)] : DecompositionMonoid α where
  primal k m n H := by
    cases h
    by_cases h0 : gcd k m = 0
    · rw [gcd_eq_zero_iff] at h0
      rcases h0 with ⟨rfl, rfl⟩
      exact ⟨0, n, dvd_refl 0, dvd_refl n, by simp⟩
    · obtain ⟨a, ha⟩ := gcd_dvd_left k m
      refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
      rw [← mul_dvd_mul_iff_left h0, ← ha]
      exact dvd_gcd_mul_of_dvd_mul H

GCD Monoid as Decomposition Monoid

Informal description

For any type $\alpha$ with a nonempty GCD monoid structure, $\alpha$ is also a decomposition monoid. This means that every element can be factored into irreducible elements in a way that respects divisibility.

gcd_mul_dvd_mul_gcd theorem

[GCDMonoid α] (k m n : α) : gcd k (m * n) ∣ gcd k m * gcd k n

Full source

theorem gcd_mul_dvd_mul_gcd [GCDMonoid α] (k m n : α) : gcdgcd k (m * n) ∣ gcd k m * gcd k n := by
  obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))
  replace h : gcd k (m * n) = m' * n' := h
  rw [h]
  have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _
  apply mul_dvd_mul
  · have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
    exact dvd_gcd hm'k hm'
  · have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
    exact dvd_gcd hn'k hn'

Divisibility of GCD over Product: $\gcd(k, m \cdot n) \mid \gcd(k, m) \cdot \gcd(k, n)$

Informal description

For any elements $k, m, n$ in a GCD monoid $\alpha$, the greatest common divisor of $k$ and $m \cdot n$ divides the product of the greatest common divisors of $k$ and $m$, and of $k$ and $n$. In other words, $\gcd(k, m \cdot n) \mid \gcd(k, m) \cdot \gcd(k, n)$.

gcd_pow_right_dvd_pow_gcd theorem

[GCDMonoid α] {a b : α} {k : ℕ} : gcd a (b ^ k) ∣ gcd a b ^ k

Full source

theorem gcd_pow_right_dvd_pow_gcd [GCDMonoid α] {a b : α} {k : ℕ} :
    gcdgcd a (b ^ k) ∣ gcd a b ^ k := by
  by_cases hg : gcd a b = 0
  · rw [gcd_eq_zero_iff] at hg
    rcases hg with ⟨rfl, rfl⟩
    exact
      (gcd_zero_left' (0 ^ k : α)).dvd.trans
        (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)
  · induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk

GCD Power Divisibility: $\gcd(a, b^k) \mid \gcd(a, b)^k$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$ and any natural number $k$, the greatest common divisor of $a$ and $b^k$ divides the $k$-th power of the greatest common divisor of $a$ and $b$, i.e., $\gcd(a, b^k) \mid (\gcd(a, b))^k$.

gcd_pow_left_dvd_pow_gcd theorem

[GCDMonoid α] {a b : α} {k : ℕ} : gcd (a ^ k) b ∣ gcd a b ^ k

Full source

theorem gcd_pow_left_dvd_pow_gcd [GCDMonoid α] {a b : α} {k : ℕ} : gcdgcd (a ^ k) b ∣ gcd a b ^ k :=
  calc
    gcd (a ^ k) b ∣ gcd b (a ^ k) := (gcd_comm' _ _).dvd
    _ ∣ gcd b a ^ kcalc
    gcd (a ^ k) b ∣ gcd b (a ^ k) := (gcd_comm' _ _).dvd
    _ ∣ gcd b a ^ k := gcd_pow_right_dvd_pow_gcd
    _ ∣ gcd a b ^ k := pow_dvd_pow_of_dvd (gcd_comm' _ _).dvd _

GCD Power Divisibility: $\gcd(a^k, b) \mid \gcd(a, b)^k$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$ and any natural number $k$, the greatest common divisor of $a^k$ and $b$ divides the $k$-th power of the greatest common divisor of $a$ and $b$, i.e., $\gcd(a^k, b) \mid (\gcd(a, b))^k$.

pow_dvd_of_mul_eq_pow theorem

 [GCDMonoid α] {a b c d₁ d₂ : α} (ha : a ≠ 0) (hab : IsUnit (gcd a b)) {k : ℕ} (h : a * b = c ^ k) (hc : c = d₁ * d₂)
  (hd₁ : d₁ ∣ a) : d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Full source

theorem pow_dvd_of_mul_eq_pow [GCDMonoid α] {a b c d₁ d₂ : α} (ha : a ≠ 0) (hab : IsUnit (gcd a b))
    {k : ℕ} (h : a * b = c ^ k) (hc : c = d₁ * d₂) (hd₁ : d₁ ∣ a) : d₁ ^ k ≠ 0d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a := by
  have h1 : IsUnit (gcd (d₁ ^ k) b) := by
    apply isUnit_of_dvd_one
    trans gcd d₁ b ^ k
    · exact gcd_pow_left_dvd_pow_gcd
    · apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      apply dvd_trans _ hab.dvd
      apply gcd_dvd_gcd hd₁ (dvd_refl b)
  have h2 : d₁ ^ k ∣ a * b := by
    use d₂ ^ k
    rw [h, hc]
    exact mul_pow d₁ d₂ k
  rw [mul_comm] at h2
  have h3 : d₁ ^ k ∣ a := by
    apply (dvd_gcd_mul_of_dvd_mul h2).trans
    rw [h1.mul_left_dvd]
  have h4 : d₁ ^ k ≠ 0 := by
    intro hdk
    rw [hdk] at h3
    apply absurd (zero_dvd_iff.mp h3) ha
  exact ⟨h4, h3⟩

Power Divisibility from Product-Power Equality in GCD Monoids: $d_1^k \mid a$ when $a \cdot b = c^k$ and $c = d_1 \cdot d_2$

Informal description

Let $\alpha$ be a GCD monoid. For any nonzero elements $a, b, c, d_1, d_2 \in \alpha$ such that: 1. $\gcd(a, b)$ is a unit, 2. $a \cdot b = c^k$ for some natural number $k$, 3. $c = d_1 \cdot d_2$ with $d_1$ dividing $a$, then $d_1^k$ is nonzero and divides $a$, i.e., $d_1^k \neq 0$ and $d_1^k \mid a$.

exists_associated_pow_of_mul_eq_pow theorem

[GCDMonoid α] {a b c : α} (hab : IsUnit (gcd a b)) {k : ℕ} (h : a * b = c ^ k) : ∃ d : α, Associated (d ^ k) a

Full source

theorem exists_associated_pow_of_mul_eq_pow [GCDMonoid α] {a b c : α} (hab : IsUnit (gcd a b))
    {k : ℕ} (h : a * b = c ^ k) : ∃ d : α, Associated (d ^ k) a := by
  cases subsingleton_or_nontrivial α
  · use 0
    rw [Subsingleton.elim a (0 ^ k)]
  by_cases ha : a = 0
  · use 0
    obtain rfl | hk := eq_or_ne k 0
    · simp [ha] at h
    · rw [ha, zero_pow hk]
  by_cases hb : b = 0
  · use 1
    rw [one_pow]
    apply (associated_one_iff_isUnit.mpr hab).symm.trans
    rw [hb]
    exact gcd_zero_right' a
  obtain rfl | hk := k.eq_zero_or_pos
  · use 1
    rw [pow_zero] at h ⊢
    use Units.mkOfMulEqOne _ _ h
    rw [Units.val_mkOfMulEqOne, one_mul]
  have hc : c ∣ a * b := by
    rw [h]
    exact dvd_pow_self _ hk.ne'
  obtain ⟨d₁, d₂, hd₁, hd₂, hc⟩ := exists_dvd_and_dvd_of_dvd_mul hc
  use d₁
  obtain ⟨h0₁, ⟨a', ha'⟩⟩ := pow_dvd_of_mul_eq_pow ha hab h hc hd₁
  rw [mul_comm] at h hc
  rw [(gcd_comm' a b).isUnit_iff] at hab
  obtain ⟨h0₂, ⟨b', hb'⟩⟩ := pow_dvd_of_mul_eq_pow hb hab h hc hd₂
  rw [ha', hb', hc, mul_pow] at h
  have h' : a' * b' = 1 := by
    apply (mul_right_inj' h0₁).mp
    rw [mul_one]
    apply (mul_right_inj' h0₂).mp
    rw [← h]
    rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
  use Units.mkOfMulEqOne _ _ h'
  rw [Units.val_mkOfMulEqOne, ha']

Existence of Associated $k$-th Power Factor in GCD Monoids: $d^k \sim a$ when $a \cdot b = c^k$ and $\gcd(a, b)$ is a unit

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b, c \in \alpha$ such that $\gcd(a, b)$ is a unit and $a \cdot b = c^k$ for some natural number $k$, there exists an element $d \in \alpha$ such that $d^k$ is associated to $a$.

exists_eq_pow_of_mul_eq_pow theorem

 [GCDMonoid α] [Subsingleton αˣ] {a b c : α} (hab : IsUnit (gcd a b)) {k : ℕ} (h : a * b = c ^ k) : ∃ d : α, a = d ^ k

Full source

theorem exists_eq_pow_of_mul_eq_pow [GCDMonoid α] [Subsingleton αˣ]
    {a b c : α} (hab : IsUnit (gcd a b)) {k : ℕ} (h : a * b = c ^ k) : ∃ d : α, a = d ^ k :=
  let ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow hab h
  ⟨d, (associated_iff_eq.mp hd).symm⟩

Existence of $k$-th Root in GCD Monoid with Unique Unit: $a = d^k$ when $a \cdot b = c^k$ and $\gcd(a, b)$ is a unit

Informal description

Let $\alpha$ be a GCD monoid with a unique unit (up to equality). For any elements $a, b, c \in \alpha$ such that $\gcd(a, b)$ is a unit and $a \cdot b = c^k$ for some natural number $k$, there exists an element $d \in \alpha$ such that $a = d^k$.

gcd_greatest theorem

 {α : Type*} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b)
  (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : GCDMonoid.gcd a b = normalize d

Full source

theorem gcd_greatest {α : Type*} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a b d : α}
    (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) :
    GCDMonoid.gcd a b = normalize d :=
  haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
  gcd_eq_normalize h (GCDMonoid.dvd_gcd hda hdb)

Greatest Common Divisor Equals Normalization of Greatest Divisor in Normalized GCD Monoid

Informal description

Let $\alpha$ be a cancellative commutative monoid with zero equipped with a normalized GCD monoid structure. For any elements $a, b, d \in \alpha$ such that $d$ divides both $a$ and $b$, and for any element $e \in \alpha$ that divides both $a$ and $b$, $e$ also divides $d$, then the greatest common divisor of $a$ and $b$ is equal to the normalization of $d$.

gcd_greatest_associated theorem

 {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b)
  (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : Associated d (GCDMonoid.gcd a b)

Full source

theorem gcd_greatest_associated {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] {a b d : α}
    (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) :
    Associated d (GCDMonoid.gcd a b) :=
  haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
  associated_of_dvd_dvd (GCDMonoid.dvd_gcd hda hdb) h

Greatest Common Divisor is Associated with Greatest Divisor in GCD Monoid

Informal description

Let $\alpha$ be a cancellative commutative monoid with zero equipped with a GCD monoid structure. For any elements $a, b, d \in \alpha$ such that $d$ divides both $a$ and $b$, and for any element $e \in \alpha$ that divides both $a$ and $b$, $e$ also divides $d$, then $d$ is associated with the greatest common divisor of $a$ and $b$.

isUnit_gcd_of_eq_mul_gcd theorem

 {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] {x y x' y' : α} (ex : x = gcd x y * x') (ey : y = gcd x y * y')
  (h : gcd x y ≠ 0) : IsUnit (gcd x' y')

Full source

theorem isUnit_gcd_of_eq_mul_gcd {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α]
    {x y x' y' : α} (ex : x = gcd x y * x') (ey : y = gcd x y * y') (h : gcdgcd x y ≠ 0) :
    IsUnit (gcd x' y') := by
  rw [← associated_one_iff_isUnit]
  refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
  convert (gcd_mul_left' (gcd x y) x' y').symm using 1
  rw [← ex, ← ey, mul_one]

GCD of Scaled Elements is Unit When Original GCD is Nonzero

Informal description

Let $\alpha$ be a cancellative commutative monoid with zero equipped with a GCD monoid structure. For any elements $x, y, x', y' \in \alpha$ such that $x = \gcd(x, y) \cdot x'$ and $y = \gcd(x, y) \cdot y'$, if $\gcd(x, y) \neq 0$, then the greatest common divisor of $x'$ and $y'$ is a unit in $\alpha$.

extract_gcd theorem

 {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] (x y : α) :
  ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

Full source

theorem extract_gcd {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] (x y : α) :
    ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y') := by
  by_cases h : gcd x y = 0
  · obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h
    simp_rw [← associated_one_iff_isUnit]
    exact ⟨1, 1, by rw [h, zero_mul], by rw [h, zero_mul], gcd_one_left' 1⟩
  obtain ⟨x', ex⟩ := gcd_dvd_left x y
  obtain ⟨y', ey⟩ := gcd_dvd_right x y
  exact ⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩

GCD Extraction Property in GCD Monoids

Informal description

Let $\alpha$ be a cancellative commutative monoid with zero equipped with a GCD monoid structure. For any elements $x, y \in \alpha$, there exist elements $x', y' \in \alpha$ such that: 1. $x = \gcd(x, y) \cdot x'$ 2. $y = \gcd(x, y) \cdot y'$ 3. The greatest common divisor of $x'$ and $y'$ is a unit in $\alpha$.

associated_gcd_left_iff theorem

[GCDMonoid α] {x y : α} : Associated x (gcd x y) ↔ x ∣ y

Full source

theorem associated_gcd_left_iff [GCDMonoid α] {x y : α} : AssociatedAssociated x (gcd x y) ↔ x ∣ y :=
  ⟨fun hx => hx.dvd.trans (gcd_dvd_right x y),
    fun hxy => associated_of_dvd_dvd (dvd_gcd dvd_rfl hxy) (gcd_dvd_left x y)⟩

Characterization of GCD Association via Divisibility

Informal description

Let $α$ be a GCD monoid. For any elements $x, y \in α$, the element $x$ is associated with the greatest common divisor of $x$ and $y$ if and only if $x$ divides $y$. In other words, $x \sim \gcd(x, y) \leftrightarrow x \mid y$.

associated_gcd_right_iff theorem

[GCDMonoid α] {x y : α} : Associated y (gcd x y) ↔ y ∣ x

Full source

theorem associated_gcd_right_iff [GCDMonoid α] {x y : α} : AssociatedAssociated y (gcd x y) ↔ y ∣ x :=
  ⟨fun hx => hx.dvd.trans (gcd_dvd_left x y),
    fun hxy => associated_of_dvd_dvd (dvd_gcd hxy dvd_rfl) (gcd_dvd_right x y)⟩

Characterization of GCD Association via Divisibility (Right Version)

Informal description

Let $α$ be a GCD monoid. For any elements $x, y \in α$, the element $y$ is associated with the greatest common divisor of $x$ and $y$ if and only if $y$ divides $x$. In other words, $y \sim \gcd(x, y) \leftrightarrow y \mid x$.

Irreducible.isUnit_gcd_iff theorem

[GCDMonoid α] {x y : α} (hx : Irreducible x) : IsUnit (gcd x y) ↔ ¬(x ∣ y)

Full source

theorem Irreducible.isUnit_gcd_iff [GCDMonoid α] {x y : α} (hx : Irreducible x) :
    IsUnitIsUnit (gcd x y) ↔ ¬(x ∣ y) := by
  rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]

Irreducible Element GCD Unit Criterion: $\gcd(x, y)$ is a unit $\leftrightarrow x \nmid y$

Informal description

Let $α$ be a GCD monoid and let $x, y \in α$ with $x$ irreducible. Then the greatest common divisor $\gcd(x, y)$ is a unit if and only if $x$ does not divide $y$. That is, $\gcd(x, y)$ is a unit $\leftrightarrow x \nmid y$.

Irreducible.gcd_eq_one_iff theorem

[NormalizedGCDMonoid α] {x y : α} (hx : Irreducible x) : gcd x y = 1 ↔ ¬(x ∣ y)

Full source

theorem Irreducible.gcd_eq_one_iff [NormalizedGCDMonoid α] {x y : α} (hx : Irreducible x) :
    gcdgcd x y = 1 ↔ ¬(x ∣ y) := by
  rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]

Irreducible Element GCD Unit Criterion in Normalized GCD Monoid: $\gcd(x, y) = 1 \leftrightarrow x \nmid y$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any irreducible element $x \in \alpha$ and any element $y \in \alpha$, the greatest common divisor $\gcd(x, y)$ equals $1$ if and only if $x$ does not divide $y$.

gcd_neg' theorem

[GCDMonoid α] {a b : α} : Associated (gcd a (-b)) (gcd a b)

Full source

lemma gcd_neg' [GCDMonoid α] {a b : α} : Associated (gcd a (-b)) (gcd a b) :=
  Associated.gcd .rfl (.neg_left .rfl)

GCD Negation Invariance up to Associated Elements: $\gcd(a, -b) \sim \gcd(a, b)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b \in \alpha$, the greatest common divisor $\gcd(a, -b)$ is associated to $\gcd(a, b)$.

gcd_neg theorem

[NormalizedGCDMonoid α] {a b : α} : gcd a (-b) = gcd a b

Full source

lemma gcd_neg [NormalizedGCDMonoid α] {a b : α} : gcd a (-b) = gcd a b :=
  gcd_neg'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)

GCD Invariance Under Negation: $\gcd(a, -b) = \gcd(a, b)$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the greatest common divisor satisfies $\gcd(a, -b) = \gcd(a, b)$.

neg_gcd' theorem

[GCDMonoid α] {a b : α} : Associated (gcd (-a) b) (gcd a b)

Full source

lemma neg_gcd' [GCDMonoid α] {a b : α} : Associated (gcd (-a) b) (gcd a b) :=
  Associated.gcd (.neg_left .rfl) .rfl

GCD of Negated Element is Associated to GCD of Original Element

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b \in \alpha$, the greatest common divisor $\gcd(-a, b)$ is associated to $\gcd(a, b)$.

neg_gcd theorem

[NormalizedGCDMonoid α] {a b : α} : gcd (-a) b = gcd a b

Full source

lemma neg_gcd [NormalizedGCDMonoid α] {a b : α} : gcd (-a) b = gcd a b :=
  neg_gcd'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)

GCD Invariance Under Negation of First Argument: $\gcd(-a, b) = \gcd(a, b)$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the greatest common divisor satisfies $\gcd(-a, b) = \gcd(a, b)$.

lcm_dvd_iff theorem

[GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Full source

theorem lcm_dvd_iff [GCDMonoid α] {a b c : α} : lcmlcm a b ∣ clcm a b ∣ c ↔ a ∣ c ∧ b ∣ c := by
  by_cases h : a = 0 ∨ b = 0
  · rcases h with (rfl | rfl) <;>
      simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
        zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true, imp_true_iff]
  · obtain ⟨h1, h2⟩ := not_or.1 h
    have h : gcdgcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
    rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]

Divisibility Characterization of LCM: $\mathrm{lcm}(a, b) \mid c \leftrightarrow a \mid c \land b \mid c$

Informal description

For any elements $a$, $b$, and $c$ in a GCD monoid $\alpha$, the least common multiple $\mathrm{lcm}(a, b)$ divides $c$ if and only if both $a$ and $b$ divide $c$.

dvd_lcm_left theorem

[GCDMonoid α] (a b : α) : a ∣ lcm a b

Full source

theorem dvd_lcm_left [GCDMonoid α] (a b : α) : a ∣ lcm a b :=
  (lcm_dvd_iff.1 (dvd_refl (lcm a b))).1

Left Divisibility of Least Common Multiple: $a \mid \mathrm{lcm}(a, b)$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the element $a$ divides the least common multiple $\mathrm{lcm}(a, b)$.

dvd_lcm_right theorem

[GCDMonoid α] (a b : α) : b ∣ lcm a b

Full source

theorem dvd_lcm_right [GCDMonoid α] (a b : α) : b ∣ lcm a b :=
  (lcm_dvd_iff.1 (dvd_refl (lcm a b))).2

Right Divisibility Property of LCM: $b \mid \mathrm{lcm}(a, b)$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the element $b$ divides the least common multiple $\mathrm{lcm}(a, b)$.

lcm_dvd theorem

[GCDMonoid α] {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b

Full source

theorem lcm_dvd [GCDMonoid α] {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcmlcm a c ∣ b :=
  lcm_dvd_iff.2 ⟨hab, hcb⟩

Least Common Multiple Divides Common Multiple: $\mathrm{lcm}(a, c) \mid b$ when $a \mid b$ and $c \mid b$

Informal description

For any elements $a$, $b$, and $c$ in a GCD monoid $\alpha$, if $a$ divides $b$ and $c$ divides $b$, then the least common multiple of $a$ and $c$ divides $b$, i.e., $\mathrm{lcm}(a, c) \mid b$.

lcm_eq_zero_iff theorem

[GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0

Full source

@[simp]
theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcmlcm a b = 0 ↔ a = 0 ∨ b = 0 :=
  Iff.intro
    (fun h : lcm a b = 0 => by
      have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
      rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero])
    (by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right])

Zero LCM Criterion in GCD Monoids: $\mathrm{lcm}(a, b) = 0 \leftrightarrow a = 0 \lor b = 0$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the least common multiple $\mathrm{lcm}(a, b)$ equals zero if and only if either $a$ is zero or $b$ is zero. That is, $\mathrm{lcm}(a, b) = 0 \leftrightarrow a = 0 \lor b = 0$.

normalize_lcm theorem

[NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b

Full source

@[simp]
theorem normalize_lcm [NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b :=
  NormalizedGCDMonoid.normalize_lcm a b

Normalization of Least Common Multiple in Normalized GCD Monoid

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the normalization of their least common multiple equals the least common multiple itself, i.e., $\text{normalize}(\text{lcm}(a, b)) = \text{lcm}(a, b)$.

lcm_comm theorem

[NormalizedGCDMonoid α] (a b : α) : lcm a b = lcm b a

Full source

theorem lcm_comm [NormalizedGCDMonoid α] (a b : α) : lcm a b = lcm b a :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

Commutativity of Least Common Multiple: $\mathrm{lcm}(a, b) = \mathrm{lcm}(b, a)$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the least common multiple of $a$ and $b$ is equal to the least common multiple of $b$ and $a$, i.e., $\mathrm{lcm}(a, b) = \mathrm{lcm}(b, a)$.

lcm_comm' theorem

[GCDMonoid α] (a b : α) : Associated (lcm a b) (lcm b a)

Full source

theorem lcm_comm' [GCDMonoid α] (a b : α) : Associated (lcm a b) (lcm b a) :=
  associated_of_dvd_dvd (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

Commutativity of Least Common Multiple up to Association: $\mathrm{lcm}(a, b) \sim \mathrm{lcm}(b, a)$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the least common multiples $\mathrm{lcm}(a, b)$ and $\mathrm{lcm}(b, a)$ are associated, meaning they differ by multiplication by a unit.

lcm_assoc theorem

[NormalizedGCDMonoid α] (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k)

Full source

theorem lcm_assoc [NormalizedGCDMonoid α] (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k) :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
    (lcm_dvd (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
      ((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
    (lcm_dvd ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
      (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))

Associativity of Least Common Multiple in Normalized GCD Monoid

Informal description

For any elements $m$, $n$, and $k$ in a normalized GCD monoid $\alpha$, the least common multiple satisfies the associativity property: \[ \mathrm{lcm}(\mathrm{lcm}(m, n), k) = \mathrm{lcm}(m, \mathrm{lcm}(n, k)). \]

lcm_assoc' theorem

[GCDMonoid α] (m n k : α) : Associated (lcm (lcm m n) k) (lcm m (lcm n k))

Full source

theorem lcm_assoc' [GCDMonoid α] (m n k : α) : Associated (lcm (lcm m n) k) (lcm m (lcm n k)) :=
  associated_of_dvd_dvd
    (lcm_dvd (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
      ((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
    (lcm_dvd ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
      (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))

Associativity of Least Common Multiple up to Unit Factor: $\mathrm{lcm}(\mathrm{lcm}(m, n), k) \sim \mathrm{lcm}(m, \mathrm{lcm}(n, k))$

Informal description

For any elements $m$, $n$, and $k$ in a GCD monoid $\alpha$, the least common multiple $\mathrm{lcm}(\mathrm{lcm}(m, n), k)$ is associated with $\mathrm{lcm}(m, \mathrm{lcm}(n, k))$. Here, two elements are *associated* if they differ by a unit factor.

instCommutativeLcm instance

[NormalizedGCDMonoid α] : Std.Commutative (α := α) lcm

Full source

instance [NormalizedGCDMonoid α] : Std.Commutative (α := α) lcm where
  comm := lcm_comm

Commutativity of Least Common Multiple in Normalized GCD Monoids

Informal description

For any normalized GCD monoid $\alpha$, the least common multiple operation $\mathrm{lcm}$ is commutative.

instAssociativeLcm instance

[NormalizedGCDMonoid α] : Std.Associative (α := α) lcm

Full source

instance [NormalizedGCDMonoid α] : Std.Associative (α := α) lcm where
  assoc := lcm_assoc

Associativity of Least Common Multiple in Normalized GCD Monoids

Informal description

For any normalized GCD monoid $\alpha$, the least common multiple operation $\mathrm{lcm}$ is associative. That is, for any elements $x, y, z \in \alpha$, we have: \[ \mathrm{lcm}(\mathrm{lcm}(x, y), z) = \mathrm{lcm}(x, \mathrm{lcm}(y, z)). \]

lcm_eq_normalize theorem

[NormalizedGCDMonoid α] {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) : lcm a b = normalize c

Full source

theorem lcm_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : lcmlcm a b ∣ c)
    (hcab : c ∣ lcm a b) : lcm a b = normalize c :=
  normalize_lcm a b ▸ normalize_eq_normalize habc hcab

Least Common Multiple Equals Normalization of Associated Element

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$, if the least common multiple $\text{lcm}(a, b)$ divides $c$ and $c$ divides $\text{lcm}(a, b)$, then $\text{lcm}(a, b)$ is equal to the normalized form of $c$, i.e., $\text{lcm}(a, b) = \text{normalize}(c)$.

lcm_dvd_lcm theorem

[GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣ lcm b d

Full source

theorem lcm_dvd_lcm [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcmlcm a c ∣ lcm b d :=
  lcm_dvd (hab.trans (dvd_lcm_left _ _)) (hcd.trans (dvd_lcm_right _ _))

Least Common Multiple Preserves Divisibility: $\mathrm{lcm}(a, c) \mid \mathrm{lcm}(b, d)$ when $a \mid b$ and $c \mid d$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b, c, d \in \alpha$ such that $a$ divides $b$ and $c$ divides $d$, the least common multiple $\mathrm{lcm}(a, c)$ divides $\mathrm{lcm}(b, d)$.

Associated.lcm theorem

 [GCDMonoid α] {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) : Associated (lcm a₁ b₁) (lcm a₂ b₂)

Full source

protected theorem Associated.lcm [GCDMonoid α]
    {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
    Associated (lcm a₁ b₁) (lcm a₂ b₂) :=
  associated_of_dvd_dvd (lcm_dvd_lcm ha.dvd hb.dvd) (lcm_dvd_lcm ha.dvd' hb.dvd')

Association of Least Common Multiples under Associated Elements

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a_1, a_2, b_1, b_2 \in \alpha$ such that $a_1$ is associated to $a_2$ and $b_1$ is associated to $b_2$, the least common multiples $\mathrm{lcm}(a_1, b_1)$ and $\mathrm{lcm}(a_2, b_2)$ are also associated.

lcm_units_coe_left theorem

[NormalizedGCDMonoid α] (u : αˣ) (a : α) : lcm (↑u) a = normalize a

Full source

@[simp]
theorem lcm_units_coe_left [NormalizedGCDMonoid α] (u : αˣ) (a : α) : lcm (↑u) a = normalize a :=
  lcm_eq_normalize (lcm_dvd Units.coe_dvd dvd_rfl) (dvd_lcm_right _ _)

Least Common Multiple with Unit on the Left Equals Normalization

Informal description

Let $\alpha$ be a normalized GCD monoid. For any unit $u$ in $\alpha$ and any element $a \in \alpha$, the least common multiple of $u$ and $a$ is equal to the normalized form of $a$, i.e., $\mathrm{lcm}(u, a) = \mathrm{normalize}(a)$.

lcm_units_coe_right theorem

[NormalizedGCDMonoid α] (a : α) (u : αˣ) : lcm a ↑u = normalize a

Full source

@[simp]
theorem lcm_units_coe_right [NormalizedGCDMonoid α] (a : α) (u : αˣ) : lcm a ↑u = normalize a :=
  (lcm_comm a u).trans <| lcm_units_coe_left _ _

Least Common Multiple with Unit on the Right Equals Normalization

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$ and any unit $u \in \alpha^\times$, the least common multiple of $a$ and $u$ is equal to the normalized form of $a$, i.e., $\mathrm{lcm}(a, u) = \mathrm{normalize}(a)$.

lcm_one_left theorem

[NormalizedGCDMonoid α] (a : α) : lcm 1 a = normalize a

Full source

@[simp]
theorem lcm_one_left [NormalizedGCDMonoid α] (a : α) : lcm 1 a = normalize a :=
  lcm_units_coe_left 1 a

Least Common Multiple with One on the Left Equals Normalization

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$, the least common multiple of $1$ and $a$ equals the normalized form of $a$, i.e., $\mathrm{lcm}(1, a) = \mathrm{normalize}(a)$.

lcm_one_right theorem

[NormalizedGCDMonoid α] (a : α) : lcm a 1 = normalize a

Full source

@[simp]
theorem lcm_one_right [NormalizedGCDMonoid α] (a : α) : lcm a 1 = normalize a :=
  lcm_units_coe_right a 1

Least Common Multiple with One on the Right Equals Normalization

Informal description

Let $\alpha$ be a normalized GCD monoid. For any element $a \in \alpha$, the least common multiple of $a$ and $1$ equals the normalized form of $a$, i.e., $\mathrm{lcm}(a, 1) = \mathrm{normalize}(a)$.

lcm_same theorem

[NormalizedGCDMonoid α] (a : α) : lcm a a = normalize a

Full source

@[simp]
theorem lcm_same [NormalizedGCDMonoid α] (a : α) : lcm a a = normalize a :=
  lcm_eq_normalize (lcm_dvd dvd_rfl dvd_rfl) (dvd_lcm_left _ _)

Least Common Multiple of an Element with Itself Equals Its Normalization

Informal description

For any element $a$ in a normalized GCD monoid $\alpha$, the least common multiple of $a$ with itself equals the normalized form of $a$, i.e., $\mathrm{lcm}(a, a) = \mathrm{normalize}(a)$.

lcm_eq_one_iff theorem

[NormalizedGCDMonoid α] (a b : α) : lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1

Full source

@[simp]
theorem lcm_eq_one_iff [NormalizedGCDMonoid α] (a b : α) : lcmlcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1 :=
  Iff.intro (fun eq => eq ▸ ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩) fun ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ =>
    show lcm (Units.mkOfMulEqOne a c hc.symm : α) (Units.mkOfMulEqOne b d hd.symm) = 1 by
      rw [lcm_units_coe_left, normalize_coe_units]

Characterization of LCM as One: $\mathrm{lcm}(a, b) = 1 \leftrightarrow a \mid 1 \land b \mid 1$

Informal description

For any elements $a$ and $b$ in a normalized GCD monoid $\alpha$, the least common multiple $\mathrm{lcm}(a, b)$ equals $1$ if and only if both $a$ and $b$ divide $1$.

lcm_mul_left theorem

[NormalizedGCDMonoid α] (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c

Full source

@[simp]
theorem lcm_mul_left [NormalizedGCDMonoid α] (a b c : α) :
    lcm (a * b) (a * c) = normalize a * lcm b c :=
  (by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]))
    fun ha : a ≠ 0 =>
    suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa
    have : a ∣ lcm (a * b) (a * c) := (dvd_mul_right _ _).trans (dvd_lcm_left _ _)
    let ⟨_, eq⟩ := this
    lcm_eq_normalize
      (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
      (eq.symm ▸
        (mul_dvd_mul_left a <|
          lcm_dvd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_left _ _)
            ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_right _ _)))

Left Multiplication Property of LCM in Normalized GCD Monoid: $\mathrm{lcm}(a b, a c) = \mathrm{normalize}(a) \cdot \mathrm{lcm}(b, c)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$, the least common multiple of $a \cdot b$ and $a \cdot c$ equals the product of the normalized form of $a$ with the least common multiple of $b$ and $c$, i.e., \[ \mathrm{lcm}(a \cdot b, a \cdot c) = \mathrm{normalize}(a) \cdot \mathrm{lcm}(b, c). \]

lcm_mul_right theorem

[NormalizedGCDMonoid α] (a b c : α) : lcm (b * a) (c * a) = lcm b c * normalize a

Full source

@[simp]
theorem lcm_mul_right [NormalizedGCDMonoid α] (a b c : α) :
    lcm (b * a) (c * a) = lcm b c * normalize a := by simp only [mul_comm, lcm_mul_left]

Right Multiplication Property of LCM in Normalized GCD Monoid: $\mathrm{lcm}(b a, c a) = \mathrm{lcm}(b, c) \cdot \mathrm{normalize}(a)$

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $a, b, c \in \alpha$, the least common multiple of $b \cdot a$ and $c \cdot a$ equals the product of the least common multiple of $b$ and $c$ with the normalized form of $a$, i.e., \[ \mathrm{lcm}(b \cdot a, c \cdot a) = \mathrm{lcm}(b, c) \cdot \mathrm{normalize}(a). \]

lcm_eq_left_iff theorem

[NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a

Full source

theorem lcm_eq_left_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) :
    lcmlcm a b = a ↔ b ∣ a :=
  (Iff.intro fun eq => eq ▸ dvd_lcm_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _)

Characterization of LCM Equality: $\text{lcm}(a, b) = a \leftrightarrow b \mid a$ for Normalized $a$

Informal description

Let $\alpha$ be a normalized GCD monoid, and let $a, b \in \alpha$ such that $a$ is normalized (i.e., $\text{normalize}(a) = a$). Then the least common multiple of $a$ and $b$ equals $a$ if and only if $b$ divides $a$, i.e., $\text{lcm}(a, b) = a \leftrightarrow b \mid a$.

lcm_eq_right_iff theorem

[NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b

Full source

theorem lcm_eq_right_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) :
    lcmlcm a b = b ↔ a ∣ b := by simpa only [lcm_comm b a] using lcm_eq_left_iff b a h

Characterization of LCM Equality: $\text{lcm}(a, b) = b \leftrightarrow a \mid b$ for Normalized $b$

Informal description

Let $\alpha$ be a normalized GCD monoid, and let $a, b \in \alpha$ such that $b$ is normalized (i.e., $\text{normalize}(b) = b$). Then the least common multiple of $a$ and $b$ equals $b$ if and only if $a$ divides $b$, i.e., $\text{lcm}(a, b) = b \leftrightarrow a \mid b$.

lcm_dvd_lcm_mul_left theorem

[GCDMonoid α] (m n k : α) : lcm m n ∣ lcm (k * m) n

Full source

theorem lcm_dvd_lcm_mul_left [GCDMonoid α] (m n k : α) : lcmlcm m n ∣ lcm (k * m) n :=
  lcm_dvd_lcm (dvd_mul_left _ _) dvd_rfl

Divisibility of LCM by Left Multiplication: $\mathrm{lcm}(m, n) \mid \mathrm{lcm}(k \cdot m, n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the least common multiple $\mathrm{lcm}(m, n)$ divides $\mathrm{lcm}(k \cdot m, n)$.

lcm_dvd_lcm_mul_right theorem

[GCDMonoid α] (m n k : α) : lcm m n ∣ lcm (m * k) n

Full source

theorem lcm_dvd_lcm_mul_right [GCDMonoid α] (m n k : α) : lcmlcm m n ∣ lcm (m * k) n :=
  lcm_dvd_lcm (dvd_mul_right _ _) dvd_rfl

Least Common Multiple Divisibility Under Right Multiplication: $\mathrm{lcm}(m, n) \mid \mathrm{lcm}(m \cdot k, n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the least common multiple $\mathrm{lcm}(m, n)$ divides $\mathrm{lcm}(m \cdot k, n)$.

lcm_dvd_lcm_mul_left_right theorem

[GCDMonoid α] (m n k : α) : lcm m n ∣ lcm m (k * n)

Full source

theorem lcm_dvd_lcm_mul_left_right [GCDMonoid α] (m n k : α) : lcmlcm m n ∣ lcm m (k * n) :=
  lcm_dvd_lcm dvd_rfl (dvd_mul_left _ _)

Least Common Multiple Preserves Divisibility Under Right Multiplication: $\mathrm{lcm}(m, n) \mid \mathrm{lcm}(m, k \cdot n)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the least common multiple $\mathrm{lcm}(m, n)$ divides $\mathrm{lcm}(m, k \cdot n)$.

lcm_dvd_lcm_mul_right_right theorem

[GCDMonoid α] (m n k : α) : lcm m n ∣ lcm m (n * k)

Full source

theorem lcm_dvd_lcm_mul_right_right [GCDMonoid α] (m n k : α) : lcmlcm m n ∣ lcm m (n * k) :=
  lcm_dvd_lcm dvd_rfl (dvd_mul_right _ _)

Least Common Multiple Divides Right-Multiplication Variant: $\mathrm{lcm}(m, n) \mid \mathrm{lcm}(m, n \cdot k)$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $m, n, k \in \alpha$, the least common multiple $\mathrm{lcm}(m, n)$ divides $\mathrm{lcm}(m, n \cdot k)$.

lcm_eq_of_associated_left theorem

[NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : lcm m k = lcm n k

Full source

theorem lcm_eq_of_associated_left [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) :
    lcm m k = lcm n k :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd_lcm h.dvd dvd_rfl)
    (lcm_dvd_lcm h.symm.dvd dvd_rfl)

Left LCM Invariance Under Associated Elements in Normalized GCD Monoid

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $m, n \in \alpha$ that are associated (i.e., differ by a unit), and for any element $k \in \alpha$, the least common multiple of $m$ and $k$ equals the least common multiple of $n$ and $k$, i.e., $\text{lcm}(m, k) = \text{lcm}(n, k)$.

lcm_eq_of_associated_right theorem

[NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : lcm k m = lcm k n

Full source

theorem lcm_eq_of_associated_right [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) :
    lcm k m = lcm k n :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd_lcm dvd_rfl h.dvd)
    (lcm_dvd_lcm dvd_rfl h.symm.dvd)

Least Common Multiple is Invariant under Right Association: $\text{lcm}(k, m) = \text{lcm}(k, n)$ when $m$ and $n$ are associated

Informal description

Let $\alpha$ be a normalized GCD monoid. For any elements $m, n \in \alpha$ that are associated (i.e., $m = u \cdot n$ for some unit $u$), and for any element $k \in \alpha$, the least common multiple of $k$ and $m$ equals the least common multiple of $k$ and $n$, i.e., $\text{lcm}(k, m) = \text{lcm}(k, n)$.

NormalizationMonoid.ofUniqueUnits instance

: NormalizationMonoid α

Full source

instance (priority := 100) NormalizationMonoid.ofUniqueUnits : NormalizationMonoid α where
  normUnit _ := 1
  normUnit_zero := rfl
  normUnit_mul _ _ := (mul_one 1).symm
  normUnit_coe_units _ := Subsingleton.elim _ _

Normalization Monoid Structure from Unique Units

Informal description

For any commutative monoid with zero and cancellation $\alpha$ that has a unique unit (up to association), there exists a canonical normalization monoid structure on $\alpha$.

uniqueNormalizationMonoidOfUniqueUnits instance

: Unique (NormalizationMonoid α)

Full source

instance uniqueNormalizationMonoidOfUniqueUnits : Unique (NormalizationMonoid α) where
  default := .ofUniqueUnits
  uniq := fun ⟨u, _, _, _⟩ => by congr; simp [eq_iff_true_of_subsingleton]

Uniqueness of Normalization Monoid Structure for Monoids with Unique Units

Informal description

For any commutative monoid with zero and cancellation $\alpha$ that has a unique unit (up to association), there exists a unique normalization monoid structure on $\alpha$.

subsingleton_gcdMonoid_of_unique_units instance

: Subsingleton (GCDMonoid α)

Full source

instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
  ⟨fun g₁ g₂ => by
    have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
    have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
    cases g₁
    cases g₂
    dsimp only at hgcd hlcm
    simp only [hgcd, hlcm]⟩

Uniqueness of GCD Monoid Structure for Monoids with Unique Units

Informal description

For any commutative monoid with zero and cancellation $\alpha$ that has a unique unit (up to association), there is at most one GCD monoid structure on $\alpha$.

subsingleton_normalizedGCDMonoid_of_unique_units instance

: Subsingleton (NormalizedGCDMonoid α)

Full source

instance subsingleton_normalizedGCDMonoid_of_unique_units : Subsingleton (NormalizedGCDMonoid α) :=
  ⟨by
    intro a b
    cases a; rename_i a_norm a_gcd _ _
    cases b; rename_i b_norm b_gcd _ _
    have := Subsingleton.elim a_gcd b_gcd
    subst this
    have := Subsingleton.elim a_norm b_norm
    subst this
    rfl⟩

Uniqueness of Normalized GCD Monoid Structure for Monoids with Unique Units

Informal description

For any commutative monoid with zero and cancellation $\alpha$ that has a unique unit (up to association), there is at most one normalized GCD monoid structure on $\alpha$.

normUnit_eq_one theorem

(x : α) : normUnit x = 1

Full source

@[simp]
theorem normUnit_eq_one (x : α) : normUnit x = 1 :=
  rfl

Normalization Unit Equals Identity in Normalization Monoids

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalization unit of $x$ equals the multiplicative identity, i.e., $\text{normUnit}(x) = 1$.

normalize_eq theorem

(x : α) : normalize x = x

Full source

@[simp]
theorem normalize_eq (x : α) : normalize x = x :=
  mul_one x

Normalization Identity: $\text{normalize}(x) = x$

Informal description

For any element $x$ in a normalization monoid $\alpha$, the normalized form of $x$ is equal to $x$ itself, i.e., $\text{normalize}(x) = x$.

associatesEquivOfUniqueUnits definition

: Associates α ≃* α

Full source

/-- If a monoid's only unit is `1`, then it is isomorphic to its associates. -/
@[simps]
def associatesEquivOfUniqueUnits : AssociatesAssociates α ≃* α where
  toFun := Associates.out
  invFun := Associates.mk
  left_inv := Associates.mk_out
  right_inv _ := (Associates.out_mk _).trans <| normalize_eq _
  map_mul' := Associates.out_mul

Multiplicative equivalence between associates and base monoid for unique units

Informal description

The multiplicative equivalence between the associates of a monoid $\alpha$ and $\alpha$ itself, when the monoid has only one unit (up to association). The function maps an associate class to its normalized representative, and the inverse function maps an element to its associate class. This equivalence preserves multiplication.

gcd_eq_of_dvd_sub_right theorem

{a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c

Full source

theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c := by
  apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
    rw [dvd_gcd_iff] <;>
    refine ⟨gcd_dvd_left _ _, ?_⟩
  · rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a b with ⟨e, he⟩
    rcases gcd_dvd_left a b with ⟨f, hf⟩
    use e - f * d
    rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
  · rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a c with ⟨e, he⟩
    rcases gcd_dvd_left a c with ⟨f, hf⟩
    use e + f * d
    rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]

GCD Equality under Divisibility of Difference: $\gcd(a, b) = \gcd(a, c)$ when $a \mid b - c$

Informal description

Let $\alpha$ be a GCD monoid. For any elements $a, b, c \in \alpha$, if $a$ divides $b - c$, then $\gcd(a, b) = \gcd(a, c)$.

gcd_eq_of_dvd_sub_left theorem

{a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a

Full source

theorem gcd_eq_of_dvd_sub_left {a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a := by
  rw [gcd_comm _ a, gcd_comm _ a, gcd_eq_of_dvd_sub_right h]

GCD Equality under Divisibility of Difference (Left Version): $\gcd(b, a) = \gcd(c, a)$ when $a \mid b - c$

Informal description

For any elements $a, b, c$ in a normalized GCD monoid $\alpha$, if $a$ divides the difference $b - c$, then the greatest common divisor $\gcd(b, a)$ is equal to $\gcd(c, a)$.

normalizationMonoidOfMonoidHomRightInverse definition

[DecidableEq α] (f : Associates α →* α) (hinv : Function.RightInverse f Associates.mk) : NormalizationMonoid α

Full source

/-- Define `NormalizationMonoid` on a structure from a `MonoidHom` inverse to `Associates.mk`. -/
def normalizationMonoidOfMonoidHomRightInverse [DecidableEq α] (f : AssociatesAssociates α →* α)
    (hinv : Function.RightInverse f Associates.mk) :
    NormalizationMonoid α where
  normUnit a :=
    if a = 0 then 1
    else Classical.choose (Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm)
  normUnit_zero := if_pos rfl
  normUnit_mul {a b} ha hb := by
    simp_rw [if_neg (mul_ne_zero ha hb), if_neg ha, if_neg hb, Units.ext_iff, Units.val_mul]
    suffices a * b * ↑(Classical.choose (associated_map_mk hinv (a * b))) =
        a * ↑(Classical.choose (associated_map_mk hinv a)) *
        (b * ↑(Classical.choose (associated_map_mk hinv b))) by
      apply mul_left_cancel₀ (mul_ne_zero ha hb) _
      simpa only [mul_assoc, mul_comm, mul_left_comm] using this
    rw [map_mk_unit_aux hinv a, map_mk_unit_aux hinv (a * b), map_mk_unit_aux hinv b, ←
      MonoidHom.map_mul, Associates.mk_mul_mk]
  normUnit_coe_units u := by
    nontriviality α
    simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]
    apply mul_left_cancel₀ (Units.ne_zero u)
    rw [Units.mul_inv, map_mk_unit_aux hinv u,
      Associates.mk_eq_mk_iff_associated.2 (associated_one_iff_isUnit.2 ⟨u, rfl⟩),
      Associates.mk_one, MonoidHom.map_one]

Normalization monoid from a right inverse monoid homomorphism

Informal description

Given a commutative monoid with zero $\alpha$ and decidable equality, and a monoid homomorphism $f$ from the monoid of associates of $\alpha$ to $\alpha$ that is a right inverse of the canonical map $\text{Associates.mk} : \alpha \to \text{Associates}\ \alpha$, this constructs a normalization monoid structure on $\alpha$. The normalization is defined by: - For $a = 0$, the norm unit is $1$. - For $a \neq 0$, the norm unit is chosen such that multiplying $a$ by this unit yields a normalized form, where the choice is made via the right inverse property of $f$. The normalization function $\text{normalize}$ is then an idempotent monoid homomorphism that maps elements to their normalized forms.

gcdMonoidOfGCD definition

 [DecidableEq α] (gcd : α → α → α) (gcd_dvd_left : ∀ a b, gcd a b ∣ a) (gcd_dvd_right : ∀ a b, gcd a b ∣ b)
  (dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b) : GCDMonoid α

Full source

/-- Define `GCDMonoid` on a structure just from the `gcd` and its properties. -/
noncomputable def gcdMonoidOfGCD [DecidableEq α] (gcd : α → α → α)
    (gcd_dvd_left : ∀ a b, gcd a b ∣ a) (gcd_dvd_right : ∀ a b, gcd a b ∣ b)
    (dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b) : GCDMonoid α :=
  { gcd
    gcd_dvd_left
    gcd_dvd_right
    dvd_gcd := fun {_ _ _} => dvd_gcd
    lcm := fun a b =>
      if a = 0 then 0 else Classical.choose ((gcd_dvd_left a b).trans (Dvd.intro b rfl))
    gcd_mul_lcm := fun a b => by
      split_ifs with a0
      · rw [mul_zero, a0, zero_mul]
      · rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]
    lcm_zero_left := fun _ => if_pos rfl
    lcm_zero_right := fun a => by
      split_ifs with a0
      · rfl
      have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
      have a0' : gcd a 0 ≠ 0 := by
        contrapose! a0
        rw [← associated_zero_iff_eq_zero, ← a0]
        exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _)
      apply Or.resolve_left (mul_eq_zero.1 _) a0'
      rw [h, mul_zero] }

Construction of GCD Monoid from GCD Function

Informal description

Given a type `α` with decidable equality and a function `gcd : α → α → α` satisfying: 1. `gcd a b` divides `a` for all `a, b : α`, 2. `gcd a b` divides `b` for all `a, b : α`, 3. For any `a, b, c : α`, if `a` divides both `c` and `b`, then `a` divides `gcd c b`, this constructs a `GCDMonoid` structure on `α`, where the least common multiple `lcm` is defined in terms of the given `gcd` function. The `lcm` operation satisfies the expected properties derived from the `gcd` operation.

normalizedGCDMonoidOfGCD definition

 [NormalizationMonoid α] [DecidableEq α] (gcd : α → α → α) (gcd_dvd_left : ∀ a b, gcd a b ∣ a)
  (gcd_dvd_right : ∀ a b, gcd a b ∣ b) (dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b)
  (normalize_gcd : ∀ a b, normalize (gcd a b) = gcd a b) : NormalizedGCDMonoid α

Full source

/-- Define `NormalizedGCDMonoid` on a structure just from the `gcd` and its properties. -/
noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq α] (gcd : α → α → α)
    (gcd_dvd_left : ∀ a b, gcd a b ∣ a) (gcd_dvd_right : ∀ a b, gcd a b ∣ b)
    (dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b)
    (normalize_gcd : ∀ a b, normalize (gcd a b) = gcd a b) : NormalizedGCDMonoid α :=
  { (inferInstance : NormalizationMonoid α) with
    gcd
    gcd_dvd_left
    gcd_dvd_right
    dvd_gcd := fun {_ _ _} => dvd_gcd
    normalize_gcd
    lcm := fun a b =>
      if a = 0 then 0
      else Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))
    normalize_lcm := fun a b => by
      dsimp [normalize]
      split_ifs with a0
      · exact @normalize_zero α _ _
      · have := (Classical.choose_spec
          (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))).symm
        set l := Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))
        obtain rfl | hb := eq_or_ne b 0
        · rw [mul_zero a, normalize_zero, mul_eq_zero] at this
          obtain ha | hl := this
          · apply (a0 _).elim
            rw [← zero_dvd_iff, ← ha]
            exact gcd_dvd_left _ _
          · rw [hl, zero_mul]
        have h1 : gcd a b ≠ 0 := by
          have hab : a * b ≠ 0 := mul_ne_zero a0 hb
          contrapose! hab
          rw [← normalize_eq_zero, ← this, hab, zero_mul]
        have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem]
        rw [← normalize_gcd] at this
        rwa [normalize.map_mul, normalize_gcd, mul_right_inj' h1] at h2
    gcd_mul_lcm := fun a b => by
      split_ifs with a0
      · rw [mul_zero, a0, zero_mul]
      · rw [← Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (.intro b rfl)))]
        exact normalize_associated (a * b)
    lcm_zero_left := fun _ => if_pos rfl
    lcm_zero_right := fun a => by
      split_ifs with a0
      · rfl
      rw [← normalize_eq_zero] at a0
      have h :=
        (Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a 0).trans (.intro 0 rfl)))).symm
      have gcd0 : gcd a 0 = normalize a := by
        rw [← normalize_gcd]
        exact normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a))
      rw [← gcd0] at a0
      apply Or.resolve_left (mul_eq_zero.1 _) a0
      rw [h, mul_zero, normalize_zero] }

Construction of Normalized GCD Monoid from GCD Function

Informal description

Given a normalization monoid $\alpha$ with decidable equality and a greatest common divisor function $\text{gcd} : \alpha \to \alpha \to \alpha$ satisfying: 1. $\text{gcd}(a, b)$ divides $a$ for all $a, b \in \alpha$, 2. $\text{gcd}(a, b)$ divides $b$ for all $a, b \in \alpha$, 3. For any $a, b, c \in \alpha$, if $a$ divides both $c$ and $b$, then $a$ divides $\text{gcd}(c, b)$, 4. $\text{normalize}(\text{gcd}(a, b)) = \text{gcd}(a, b)$ for all $a, b \in \alpha$, this constructs a `NormalizedGCDMonoid` structure on $\alpha$, where the least common multiple $\text{lcm}$ is defined in terms of the given $\text{gcd}$ function. The $\text{lcm}$ operation satisfies the expected properties derived from the $\text{gcd}$ operation, and both $\text{gcd}$ and $\text{lcm}$ are normalized.

gcdMonoidOfLCM definition

 [DecidableEq α] (lcm : α → α → α) (dvd_lcm_left : ∀ a b, a ∣ lcm a b) (dvd_lcm_right : ∀ a b, b ∣ lcm a b)
  (lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a) : GCDMonoid α

Full source

/-- Define `GCDMonoid` on a structure just from the `lcm` and its properties. -/
noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α)
    (dvd_lcm_left : ∀ a b, a ∣ lcm a b) (dvd_lcm_right : ∀ a b, b ∣ lcm a b)
    (lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a) : GCDMonoid α :=
  let exists_gcd a b := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
  { lcm
    gcd := fun a b => if a = 0 then b else if b = 0 then a else Classical.choose (exists_gcd a b)
    gcd_mul_lcm := fun a b => by
      split_ifs with h h_1
      · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
      · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
      rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
    lcm_zero_left := fun _ => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
    lcm_zero_right := fun _ => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
    gcd_dvd_left := fun a b => by
      split_ifs with h h_1
      · rw [h]
        apply dvd_zero
      · exact dvd_rfl
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm,
        mul_dvd_mul_iff_right h]
      apply dvd_lcm_right
    gcd_dvd_right := fun a b => by
      split_ifs with h h_1
      · exact dvd_rfl
      · rw [h_1]
        apply dvd_zero
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_dvd_mul_iff_right h_1]
      apply dvd_lcm_left
    dvd_gcd := fun {a b c} ac ab => by
      split_ifs with h h_1
      · exact ab
      · exact ac
      have h0 : lcm c b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹c = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]
      rcases ab with ⟨d, rfl⟩
      rw [mul_eq_zero] at ‹a * d ≠ 0›
      push_neg at h_1
      rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
      apply lcm_dvd (Dvd.intro d rfl)
      rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
      apply ac }

Construction of GCD Monoid from LCM Function

Informal description

Given a type $\alpha$ with decidable equality and a function $\text{lcm} : \alpha \to \alpha \to \alpha$ satisfying: 1. $\text{lcm}(a, b)$ is divisible by $a$ for all $a, b \in \alpha$, 2. $\text{lcm}(a, b)$ is divisible by $b$ for all $a, b \in \alpha$, 3. For any $a, b, c \in \alpha$, if $c$ divides $a$ and $b$ divides $a$, then $\text{lcm}(c, b)$ divides $a$, this constructs a `GCDMonoid` structure on $\alpha$, where the greatest common divisor $\text{gcd}$ is defined in terms of the given $\text{lcm}$ function. The $\text{gcd}$ operation satisfies the expected properties derived from the $\text{lcm}$ operation.

normalizedGCDMonoidOfLCM definition

 [NormalizationMonoid α] [DecidableEq α] (lcm : α → α → α) (dvd_lcm_left : ∀ a b, a ∣ lcm a b)
  (dvd_lcm_right : ∀ a b, b ∣ lcm a b) (lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a)
  (normalize_lcm : ∀ a b, normalize (lcm a b) = lcm a b) : NormalizedGCDMonoid α

Full source

/-- Define `NormalizedGCDMonoid` on a structure just from the `lcm` and its properties. -/
noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq α] (lcm : α → α → α)
    (dvd_lcm_left : ∀ a b, a ∣ lcm a b) (dvd_lcm_right : ∀ a b, b ∣ lcm a b)
    (lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a)
    (normalize_lcm : ∀ a b, normalize (lcm a b) = lcm a b) : NormalizedGCDMonoid α :=
  let exists_gcd a b := dvd_normalize_iff.2 (lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl))
  { (inferInstance : NormalizationMonoid α) with
    lcm
    gcd := fun a b =>
      if a = 0 then normalize b
      else if b = 0 then normalize a else Classical.choose (exists_gcd a b)
    gcd_mul_lcm := fun a b => by
      split_ifs with h h_1
      · rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
      · rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _), mul_zero, mul_zero]
      rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
      exact normalize_associated (a * b)
    normalize_lcm
    normalize_gcd := fun a b => by
      dsimp [normalize]
      split_ifs with h h_1
      · apply normalize_idem
      · apply normalize_idem
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      apply mul_left_cancel₀ h0
      refine _root_.trans ?_ (Classical.choose_spec (exists_gcd a b))
      conv_lhs =>
        congr
        rw [← normalize_lcm a b]
      rw [← normalize_apply, ← normalize.map_mul,
        ← Classical.choose_spec (exists_gcd a b), normalize_idem]
    lcm_zero_left := fun _ => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
    lcm_zero_right := fun _ => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
    gcd_dvd_left := fun a b => by
      split_ifs with h h_1
      · rw [h]
        apply dvd_zero
      · exact (normalize_associated _).dvd
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), normalize_dvd_iff,
        mul_comm, mul_dvd_mul_iff_right h]
      apply dvd_lcm_right
    gcd_dvd_right := fun a b => by
      split_ifs with h h_1
      · exact (normalize_associated _).dvd
      · rw [h_1]
        apply dvd_zero
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), normalize_dvd_iff,
        mul_dvd_mul_iff_right h_1]
      apply dvd_lcm_left
    dvd_gcd := fun {a b c} ac ab => by
      split_ifs with h h_1
      · apply dvd_normalize_iff.2 ab
      · apply dvd_normalize_iff.2 ac
      have h0 : lcm c b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹c = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec
        (dvd_normalize_iff.2 (lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl))),
      dvd_normalize_iff]
      rcases ab with ⟨d, rfl⟩
      rw [mul_eq_zero] at h_1
      push_neg at h_1
      rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
      apply lcm_dvd (Dvd.intro d rfl)
      rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
      apply ac }

Construction of Normalized GCD Monoid from LCM Function

Informal description

Given a normalization monoid $\alpha$ with decidable equality and a least common multiple function $\text{lcm} : \alpha \to \alpha \to \alpha$ satisfying: 1. $\text{lcm}(a, b)$ is divisible by $a$ for all $a, b \in \alpha$, 2. $\text{lcm}(a, b)$ is divisible by $b$ for all $a, b \in \alpha$, 3. For any $a, b, c \in \alpha$, if $c$ divides $a$ and $b$ divides $a$, then $\text{lcm}(c, b)$ divides $a$, 4. $\text{normalize}(\text{lcm}(a, b)) = \text{lcm}(a, b)$ for all $a, b \in \alpha$, this constructs a `NormalizedGCDMonoid` structure on $\alpha$, where the greatest common divisor $\text{gcd}$ is defined in terms of the given $\text{lcm}$ function. The $\text{gcd}$ operation satisfies the expected properties derived from the $\text{lcm}$ operation, and both $\text{gcd}$ and $\text{lcm}$ are normalized.

gcdMonoidOfExistsGCD definition

[DecidableEq α] (h : ∀ a b : α, ∃ c : α, ∀ d : α, d ∣ a ∧ d ∣ b ↔ d ∣ c) : GCDMonoid α

Full source

/-- Define a `GCDMonoid` structure on a monoid just from the existence of a `gcd`. -/
noncomputable def gcdMonoidOfExistsGCD [DecidableEq α]
    (h : ∀ a b : α, ∃ c : α, ∀ d : α, d ∣ a ∧ d ∣ b ↔ d ∣ c) : GCDMonoid α :=
  gcdMonoidOfGCD (fun a b => Classical.choose (h a b))
    (fun a b => ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).1)
    (fun a b => ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).2)
    fun {a b c} ac ab => (Classical.choose_spec (h c b) a).1 ⟨ac, ab⟩

Construction of GCD Monoid from Existence of GCD

Informal description

Given a cancellative commutative monoid with zero $\alpha$ and a proof that for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that for any $d \in \alpha$, $d$ divides both $a$ and $b$ if and only if $d$ divides $c$, this constructs a `GCDMonoid` structure on $\alpha$. The greatest common divisor function $\gcd$ is defined nonconstructively using the axiom of choice from the given existence property.

normalizedGCDMonoidOfExistsGCD definition

 [NormalizationMonoid α] [DecidableEq α] (h : ∀ a b : α, ∃ c : α, ∀ d : α, d ∣ a ∧ d ∣ b ↔ d ∣ c) :
  NormalizedGCDMonoid α

Full source

/-- Define a `NormalizedGCDMonoid` structure on a monoid just from the existence of a `gcd`. -/
noncomputable def normalizedGCDMonoidOfExistsGCD [NormalizationMonoid α] [DecidableEq α]
    (h : ∀ a b : α, ∃ c : α, ∀ d : α, d ∣ a ∧ d ∣ b ↔ d ∣ c) : NormalizedGCDMonoid α :=
  normalizedGCDMonoidOfGCD (fun a b => normalize (Classical.choose (h a b)))
    (fun a b =>
      normalize_dvd_iff.2 ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).1)
    (fun a b =>
      normalize_dvd_iff.2 ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).2)
    (fun {a b c} ac ab => dvd_normalize_iff.2 ((Classical.choose_spec (h c b) a).1 ⟨ac, ab⟩))
    fun _ _ => normalize_idem _

Construction of Normalized GCD Monoid from Existence of GCD

Informal description

Given a normalization monoid $\alpha$ with decidable equality and a proof that for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that for any $d \in \alpha$, $d$ divides both $a$ and $b$ if and only if $d$ divides $c$, this constructs a `NormalizedGCDMonoid` structure on $\alpha$. The greatest common divisor function $\gcd$ is defined nonconstructively as the normalized representative of the chosen element $c$ (using the axiom of choice), and it satisfies the standard properties of divisibility and normalization.

gcdMonoidOfExistsLCM definition

[DecidableEq α] (h : ∀ a b : α, ∃ c : α, ∀ d : α, a ∣ d ∧ b ∣ d ↔ c ∣ d) : GCDMonoid α

Full source

/-- Define a `GCDMonoid` structure on a monoid just from the existence of an `lcm`. -/
noncomputable def gcdMonoidOfExistsLCM [DecidableEq α]
    (h : ∀ a b : α, ∃ c : α, ∀ d : α, a ∣ d ∧ b ∣ d ↔ c ∣ d) : GCDMonoid α :=
  gcdMonoidOfLCM (fun a b => Classical.choose (h a b))
    (fun a b => ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).1)
    (fun a b => ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).2)
    fun {a b c} ac ab => (Classical.choose_spec (h c b) a).1 ⟨ac, ab⟩

Construction of GCD Monoid from Existence of LCM

Informal description

Given a type $\alpha$ with decidable equality and a proof that for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that for any $d \in \alpha$, $a$ divides $d$ and $b$ divides $d$ if and only if $c$ divides $d$, this constructs a `GCDMonoid` structure on $\alpha$. The greatest common divisor `gcd` is defined nonconstructively using the axiom of choice from the given least common multiple `lcm` property.

normalizedGCDMonoidOfExistsLCM definition

 [NormalizationMonoid α] [DecidableEq α] (h : ∀ a b : α, ∃ c : α, ∀ d : α, a ∣ d ∧ b ∣ d ↔ c ∣ d) :
  NormalizedGCDMonoid α

Full source

/-- Define a `NormalizedGCDMonoid` structure on a monoid just from the existence of an `lcm`. -/
noncomputable def normalizedGCDMonoidOfExistsLCM [NormalizationMonoid α] [DecidableEq α]
    (h : ∀ a b : α, ∃ c : α, ∀ d : α, a ∣ d ∧ b ∣ d ↔ c ∣ d) : NormalizedGCDMonoid α :=
  normalizedGCDMonoidOfLCM (fun a b => normalize (Classical.choose (h a b)))
    (fun a b =>
      dvd_normalize_iff.2 ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).1)
    (fun a b =>
      dvd_normalize_iff.2 ((Classical.choose_spec (h a b) (Classical.choose (h a b))).2 dvd_rfl).2)
    (fun {a b c} ac ab => normalize_dvd_iff.2 ((Classical.choose_spec (h c b) a).1 ⟨ac, ab⟩))
    fun _ _ => normalize_idem _

Construction of Normalized GCD Monoid from Existence of LCM

Informal description

Given a normalization monoid $\alpha$ with decidable equality and a proof that for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that for any $d \in \alpha$, $a$ divides $d$ and $b$ divides $d$ if and only if $c$ divides $d$, this constructs a `NormalizedGCDMonoid` structure on $\alpha$. The greatest common divisor `gcd` and least common multiple `lcm` are defined nonconstructively using the axiom of choice, with `lcm` normalized by the given normalization function.

CommGroupWithZero.instNormalizedGCDMonoid instance

: NormalizedGCDMonoid G₀

Full source

instance (priority := 100) : NormalizedGCDMonoid G₀ where
  normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹
  normUnit_zero := dif_pos rfl
  normUnit_mul {x y} x0 y0 := Units.eq_iff.1 (by simp [x0, y0, mul_comm])
  normUnit_coe_units u := by simp
  gcd a b := if a = 0 ∧ b = 0 then 0 else 1
  lcm a b := if a = 0 ∨ b = 0 then 0 else 1
  gcd_dvd_left a b := by simp +contextual
  gcd_dvd_right a b := by simp +contextual
  dvd_gcd {a b c} hac hab := by simp_all
  gcd_mul_lcm a b := by
    split_ifs <;> simp_all [Associated.comm]
  lcm_zero_left _ := if_pos (Or.inl rfl)
  lcm_zero_right _ := if_pos (Or.inr rfl)
  -- `split_ifs` wants to split `normalize`, so handle the cases manually
  normalize_gcd a b := if h : a = 0 ∧ b = 0 then by simp [if_pos h] else by simp [if_neg h]
  normalize_lcm a b := if h : a = 0 ∨ b = 0 then by simp [if_pos h] else by simp [if_neg h]

Commutative Groups with Zero as Normalized GCD Monoids

Informal description

Every commutative group with zero $G_0$ is a normalized GCD monoid.

CommGroupWithZero.coe_normUnit theorem

{a : G₀} (h0 : a ≠ 0) : (↑(normUnit a) : G₀) = a⁻¹

Full source

@[simp]
theorem coe_normUnit {a : G₀} (h0 : a ≠ 0) : (↑(normUnit a) : G₀) = a⁻¹ := by simp [normUnit, h0]

Coercion of Normalization Unit Equals Inverse in Commutative Group with Zero

Informal description

For any nonzero element $a$ in a commutative group with zero $G_0$, the coercion of the normalization unit of $a$ to $G_0$ equals the inverse of $a$, i.e., $\uparrow(\text{normUnit}\, a) = a^{-1}$.

CommGroupWithZero.normalize_eq_one theorem

{a : G₀} (h0 : a ≠ 0) : normalize a = 1

Full source

theorem normalize_eq_one {a : G₀} (h0 : a ≠ 0) : normalize a = 1 := by simp [normalize_apply, h0]

Normalization of Nonzero Elements Yields Identity in Commutative Group with Zero

Informal description

For any nonzero element $a$ in a commutative group with zero $G_0$, the normalization of $a$ equals the multiplicative identity, i.e., $\text{normalize}(a) = 1$.

Associates.instGCDMonoid instance

: GCDMonoid (Associates α)

Full source

instance instGCDMonoid : GCDMonoid (Associates α) where
  gcd := Quotient.map₂ gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
  lcm := Quotient.map₂ lcm fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.lcm hb
  gcd_dvd_left := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_left _ _)
  gcd_dvd_right := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_right _ _)
  dvd_gcd := by
    rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ hac hbc
    exact mk_le_mk_of_dvd (dvd_gcd (dvd_of_mk_le_mk hac) (dvd_of_mk_le_mk hbc))
  gcd_mul_lcm := by
    rintro ⟨a⟩ ⟨b⟩
    rw [associated_iff_eq]
    exact Quotient.sound <| gcd_mul_lcm _ _
  lcm_zero_left := by rintro ⟨a⟩; exact congr_arg Associates.mk <| lcm_zero_left _
  lcm_zero_right := by rintro ⟨a⟩; exact congr_arg Associates.mk <| lcm_zero_right _

GCD Monoid Structure on Associates

Informal description

The type of associates of a GCD monoid $\alpha$ forms a GCD monoid, where the greatest common divisor and least common multiple operations are inherited from $\alpha$ and respect the equivalence relation of association.

Associates.gcd_mk_mk theorem

{a b : α} : gcd (Associates.mk a) (Associates.mk b) = Associates.mk (gcd a b)

Full source

theorem gcd_mk_mk {a b : α} : gcd (Associates.mk a) (Associates.mk b) = Associates.mk (gcd a b) :=
  rfl

GCD of Associates Equals Associate of GCD

Informal description

For any two elements $a$ and $b$ in a GCD monoid $\alpha$, the greatest common divisor of their associated elements in the monoid of associates is equal to the associate of the greatest common divisor of $a$ and $b$. In other words, $\gcd(\text{mk}(a), \text{mk}(b)) = \text{mk}(\gcd(a, b))$.

Associates.lcm_mk_mk theorem

{a b : α} : lcm (Associates.mk a) (Associates.mk b) = Associates.mk (lcm a b)

Full source

theorem lcm_mk_mk {a b : α} : lcm (Associates.mk a) (Associates.mk b) = Associates.mk (lcm a b) :=
  rfl

Associates LCM Preservation: $\text{lcm}(\overline{a}, \overline{b}) = \overline{\text{lcm}(a, b)}$

Informal description

For any elements $a$ and $b$ in a GCD monoid $\alpha$, the least common multiple of their associates is equal to the associate of the least common multiple of $a$ and $b$, i.e., $\text{lcm}(\text{Associates.mk}(a), \text{Associates.mk}(b)) = \text{Associates.mk}(\text{lcm}(a, b))$.

Mathlib.Algebra.GCDMonoid.Basic

Main Definitions

Implementation Notes

TODO

Tags