Monoids with normalization functions, gcd, and lcm

This file defines extra structures on CommMonoidWithZeros.

Main Definitions

• NormalizationMonoid
• StrongNormalizationMonoid
• GCDMonoid
• IsGCDMonoid
• NormalizedGCDMonoid
• StrongNormalizedGCDMonoid
• gcdMonoidOfGCD, gcdMonoidOfExistsGCD, normalizedGCDMonoidOfGCD, normalizedGCDMonoidOfExistsGCD
• gcdMonoidOfLCM, gcdMonoidOfExistsLCM, normalizedGCDMonoidOfLCM, normalizedGCDMonoidOfExistsLCM

For the NormalizedGCDMonoid instances on ℕ and ℤ, see Mathlib/Algebra/GCDMonoid/Nat.lean.

Implementation Notes

• NormalizationMonoid is defined by assigning to each element a normUnit such that multiplying by that unit normalizes the monoid, and normalize is an idempotent function. This definition as currently implemented does casework on 0.

• StrongNormalizationMonoid further requires normalize to be a monoid homomorphism.

• GCDMonoid contains the definitions of gcd and lcm with the usual properties. They are both determined up to a unit.

• IsGCDMonoid is the predicate for the existence of a GCDMonoid structure.

• NormalizedGCDMonoid extends NormalizationMonoid, so the gcd and lcm are always normalized. This makes gcds of polynomials easier to work with, but excludes Euclidean domains, and monoids without zero.

• StrongNormalizedGCDMonoid similarly extends StrongNormalizationMonoid.

• gcdMonoidOfGCD and normalizedGCDMonoidOfGCD noncomputably construct a GCDMonoid (resp. NormalizedGCDMonoid) structure just from the gcd and its properties.

• gcdMonoidOfExistsGCD and normalizedGCDMonoidOfExistsGCD noncomputably construct a GCDMonoid (resp. NormalizedGCDMonoid) structure just from a proof that any two elements have a (not necessarily normalized) gcd.

• gcdMonoidOfLCM and normalizedGCDMonoidOfLCM noncomputably construct a GCDMonoid (resp. NormalizedGCDMonoid) structure just from the lcm and its properties.

• gcdMonoidOfExistsLCM and normalizedGCDMonoidOfExistsLCM noncomputably construct a GCDMonoid (resp. NormalizedGCDMonoid) structure just from a proof that any two elements have a (not necessarily normalized) lcm.

TODO

• Port GCD facts about nats, definition of coprime
• Generalize normalization monoids to commutative (cancellative) monoids with or without zero

Tags

divisibility, gcd, lcm, normalize

class NormalizationMonoid (α : Type u_2) [MonoidWithZero α] : Type u_2

Normalization monoid: multiplying with normUnit gives a normal form for associated elements.

• normUnit : α → αˣ

  normUnit assigns to each element of the monoid a unit of the monoid.

• normUnit_zero : normUnit 0 = 1
• normUnit_one : normUnit 1 = 1
• normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a

  The condition that ensures associated elements are normalized to the same element.

@[reducible, inline]

noncomputable abbrev NormalizationMonoid.ofRightInverse {α : Type u_2} [MonoidWithZero α] [IsLeftCancelMulZero α] (out : Associates α → α) (mk_out : ∀ (a : Associates α), Associates.mk (out a) = a) (out_one : out 1 = 1) : NormalizationMonoid α

Construct a NormalizationMonoid from a right inverse of Associates.mk.

Equations

• NormalizationMonoid.ofRightInverse out mk_out out_one = { normUnit := fun (a : α) => if a = 0 then 1 else Exists.choose ⋯, normUnit_zero := ⋯, normUnit_one := ⋯, normUnit_mul_units := ⋯ }

instance instNonemptyNormalizationMonoidOfIsLeftCancelMulZero (α : Type u_2) [MonoidWithZero α] [IsLeftCancelMulZero α] : Nonempty (NormalizationMonoid α)

A cancellative monoid with zero always admits a NormalizationMonoid structure.

class StrongNormalizationMonoid (α : Type u_2) [CommMonoidWithZero α] extends NormalizationMonoid α : Type u_2

Strong normalization monoid: multiplying with normUnit gives a normal form for associated elements. It is stronger in that it ensures the normalization map is a monoid homomorphism.

• normUnit : α → αˣ
• normUnit_zero : normUnit 0 = 1
• normUnit_one : normUnit 1 = 1
• normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a
• normUnit_mul {a b : α} : a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b

  The proposition that normUnit respects multiplication of non-zero elements.

• normUnit_coe_units (u : αˣ) : normUnit ↑u = u⁻¹

  The proposition that normUnit maps units to their inverses.

@[simp]

theorem normUnit_coe_units {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (u : αˣ) : normUnit ↑u = u⁻¹

def normalize {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : α

Chooses an element of each associate class, by multiplying by normUnit

Equations

• normalize x = x * ↑(normUnit x)

theorem associated_normalize {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : Associated x (normalize x)

theorem normalize_associated {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : Associated (normalize x) x

theorem associated_normalize_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {x y : α} : Associated x (normalize y) ↔ Associated x y

theorem normalize_associated_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {x y : α} : Associated (normalize x) y ↔ Associated x y

theorem Associates.mk_normalize {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : Associates.mk (normalize x) = Associates.mk x

theorem normalize_apply {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : normalize x = x * ↑(normUnit x)

@[simp]

theorem normalize_zero {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : normalize 0 = 0

@[simp]

theorem normalize_one {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : normalize 1 = 1

theorem normalize_coe_units {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (u : αˣ) : normalize ↑u = 1

@[simp]

theorem normalize_eq_zero {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {x : α} : normalize x = 0 ↔ x = 0

theorem normalize_eq_one {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {x : α} : normalize x = 1 ↔ IsUnit x

@[simp]

theorem normUnit_mul_normUnit {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (a : α) : normUnit (a * ↑(normUnit a)) = 1

@[simp]

theorem normalize_idem {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (x : α) : normalize (normalize x) = normalize x

theorem normalize_eq_normalize_iff_associated {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {a b : α} : normalize a = normalize b ↔ Associated a b

theorem Associated.eq_of_normalized {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {a b : α} (h : Associated a b) (ha : normalize a = a) (hb : normalize b = b) : a = b

@[simp]

theorem dvd_normalize_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {a b : α} : a ∣ normalize b ↔ a ∣ b

@[simp]

theorem normalize_dvd_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {a b : α} : normalize a ∣ b ↔ a ∣ b

theorem normalize_eq_normalize {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] [IsLeftCancelMulZero α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : normalize a = normalize b

theorem normalize_eq_normalize_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] [IsLeftCancelMulZero α] {x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x

theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] [IsLeftCancelMulZero α] {a b : α} (ha : normalize a = a) (hb : normalize b = b) (hab : a ∣ b) (hba : b ∣ a) : a = b

def Associates.out {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : Associates α → α

Maps an element of Associates back to the normalized element of its associate class

Equations

• Associates.out = Quotient.lift normalize ⋯

@[simp]

theorem Associates.out_mk {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (a : α) : (Associates.mk a).out = normalize a

@[simp]

theorem Associates.out_one {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : Associates.out 1 = 1

@[simp]

theorem Associates.out_top {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : ⊤.out = 0

@[simp]

theorem Associates.normalize_out {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (a : Associates α) : normalize a.out = a.out

@[simp]

theorem Associates.mk_out {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] (a : Associates α) : Associates.mk a.out = a

theorem Associates.out_injective {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : Function.Injective Associates.out

@[simp]

theorem Associates.out_eq_zero_iff {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] {a : Associates α} : a.out = 0 ↔ a = 0

theorem Associates.out_zero {α : Type u_1} [MonoidWithZero α] [NormalizationMonoid α] : Associates.out 0 = 0

theorem Associates.out_mul' {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] (a b : Associates α) : Associated (a * b).out (a.out * b.out)

theorem Associates.dvd_out_iff {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] (a : α) (b : Associates α) : a ∣ b.out ↔ Associates.mk a ≤ b

theorem Associates.out_dvd_iff {α : Type u_2} [CommMonoidWithZero α] [NormalizationMonoid α] (a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associates.mk a

@[simp]

theorem normalize_mul {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizationMonoid α] (x y : α) : normalize (x * y) = normalize x * normalize y

def normalizeHom {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizationMonoid α] : α →*₀ α

normalize in a StrongNormalizationMonoid as a MonoidWithZeroHom.

Equations

• normalizeHom = { toFun := normalize, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem coe_normalizeHom {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizationMonoid α] : ⇑normalizeHom = normalize

theorem Associates.out_mul {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizationMonoid α] (a b : Associates α) : (a * b).out = a.out * b.out

class GCDMonoid (α : Type u_2) [CommMonoidWithZero α] extends IsCancelMulZero α : Type u_2

GCD monoid: a cancellative CommMonoidWithZero 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.

• mul_left_cancel_of_ne_zero {a : α} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : α} : a ≠ 0 → IsRightRegular a
• gcd : α → α → α

  The greatest common divisor between two elements.

• lcm : α → α → α

  The least common multiple between two elements.

• gcd_dvd_left (a b : α) : gcd a b ∣ a

  The GCD is a divisor of the first element.

• gcd_dvd_right (a b : α) : gcd a b ∣ b

  The GCD is a divisor of the second element.

• dvd_gcd {a b c : α} : a ∣ c → a ∣ b → a ∣ gcd c b

  Any common divisor of both elements is a divisor of the GCD.

• gcd_mul_lcm (a b : α) : Associated (gcd a b * lcm a b) (a * b)

  The product of two elements is Associated with the product of their GCD and LCM.

• lcm_zero_left (a : α) : lcm 0 a = 0

  0 is left-absorbing.

• lcm_zero_right (a : α) : lcm a 0 = 0

  0 is right-absorbing.

class inductive IsGCDMonoid (α : Type u_2) [CommMonoidWithZero α] : Prop

Existence of a GCDMonoid structure on a CommMonoidWithZero.

• intro {α : Type u_2} [CommMonoidWithZero α] : ∀ (a : GCDMonoid α), IsGCDMonoid α

class NormalizedGCDMonoid (α : Type u_2) [CommMonoidWithZero α] extends NormalizationMonoid α, GCDMonoid α : Type u_2

Normalized GCD monoid: a cancellative CommMonoidWithZero 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.

• normUnit : α → αˣ
• normUnit_zero : normUnit 0 = 1
• normUnit_one : normUnit 1 = 1
• normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a
• mul_left_cancel_of_ne_zero {a : α} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : α} : a ≠ 0 → IsRightRegular a
• gcd : α → α → α
• lcm : α → α → α
• 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
• gcd_mul_lcm (a b : α) : Associated (gcd a b * lcm a b) (a * b)
• lcm_zero_left (a : α) : lcm 0 a = 0
• lcm_zero_right (a : α) : lcm a 0 = 0
• normalize_gcd (a b : α) : normalize (gcd a b) = gcd a b

  The GCD is normalized to itself.

• normalize_lcm (a b : α) : normalize (lcm a b) = lcm a b

  The LCM is normalized to itself.

class StrongNormalizedGCDMonoid (α : Type u_2) [CommMonoidWithZero α] extends StrongNormalizationMonoid α, GCDMonoid α : Type u_2

Strong normalized GCD monoid: a NormalizedGCDMonoid whose normalize function is a monoid homomorphism.

• normUnit : α → αˣ
• normUnit_zero : normUnit 0 = 1
• normUnit_one : normUnit 1 = 1
• normUnit_mul_units {a : α} (u : αˣ) : a ≠ 0 → normUnit (a * ↑u) = u⁻¹ * normUnit a
• normUnit_mul {a b : α} : a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
• normUnit_coe_units (u : αˣ) : normUnit ↑u = u⁻¹
• mul_left_cancel_of_ne_zero {a : α} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : α} : a ≠ 0 → IsRightRegular a
• gcd : α → α → α
• lcm : α → α → α
• 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
• gcd_mul_lcm (a b : α) : Associated (gcd a b * lcm a b) (a * b)
• lcm_zero_left (a : α) : lcm 0 a = 0
• lcm_zero_right (a : α) : lcm a 0 = 0
• normalize_gcd (a b : α) : normalize (gcd a b) = gcd a b

  The GCD is normalized to itself.

• normalize_lcm (a b : α) : normalize (lcm a b) = lcm a b

  The LCM is normalized to itself.

@[implicit_reducible]

instance instNormalizedGCDMonoidOfStrongNormalizedGCDMonoid (α : Type u_2) [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] : NormalizedGCDMonoid α

Equations

• instNormalizedGCDMonoidOfStrongNormalizedGCDMonoid α = { toNormalizationMonoid := inst✝.toNormalizationMonoid, toGCDMonoid := inst✝.toGCDMonoid, normalize_gcd := ⋯, normalize_lcm := ⋯ }

instance instNonemptyNormalizationMonoid {α : Type u_1} [CommMonoidWithZero α] [NormalizationMonoid α] : Nonempty (NormalizationMonoid α)

instance instNonemptyStrongNormalizationMonoid {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizationMonoid α] : Nonempty (StrongNormalizationMonoid α)

@[instance 100]

instance instIsGCDMonoidOfGCDMonoid {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] : IsGCDMonoid α

theorem IsGCDMonoid.isCancelMulZero (α : Type u_1) [CommMonoidWithZero α] [h : IsGCDMonoid α] : IsCancelMulZero α

theorem gcd_isUnit_iff_isRelPrime {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} : IsUnit (gcd a b) ↔ IsRelPrime a b

@[simp]

theorem normalize_gcd {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) : normalize (gcd a b) = gcd a b

theorem dvd_gcd_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b c : α) : a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c

theorem gcd_comm {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) : gcd a b = gcd b a

theorem gcd_comm' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : Associated (gcd a b) (gcd b a)

theorem gcd_assoc {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k)

theorem gcd_assoc' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (gcd m (gcd n k))

instance instCommutativeGcd {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] : Std.Commutative gcd

instance instAssociativeGcd {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] : Std.Associative gcd

theorem gcd_eq_normalize {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) : gcd a b = normalize c

@[simp]

theorem gcd_zero_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : gcd 0 a = normalize a

theorem gcd_zero_left' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : Associated (gcd 0 a) a

@[simp]

theorem gcd_zero_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : gcd a 0 = normalize a

theorem gcd_zero_right' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : Associated (gcd a 0) a

@[simp]

theorem gcd_eq_zero_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0

theorem gcd_ne_zero_of_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (ha : a ≠ 0) : gcd a b ≠ 0

theorem gcd_ne_zero_of_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (hb : b ≠ 0) : gcd a b ≠ 0

@[simp]

theorem gcd_one_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : gcd 1 a = 1

@[simp]

theorem isUnit_gcd_one_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : IsUnit (gcd 1 a)

theorem gcd_one_left' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : Associated (gcd 1 a) 1

@[simp]

theorem gcd_one_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : gcd a 1 = 1

@[simp]

theorem isUnit_gcd_one_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : IsUnit (gcd a 1)

theorem gcd_one_right' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a : α) : Associated (gcd a 1) 1

theorem gcd_dvd_gcd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d

theorem Associated.gcd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) : Associated (gcd a₁ b₁) (gcd a₂ b₂)

@[simp]

theorem gcd_same {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : gcd a a = normalize a

@[simp]

theorem gcd_mul_left {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c

theorem gcd_mul_left' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b c : α) : Associated (gcd (a * b) (a * c)) (a * gcd b c)

@[simp]

theorem gcd_mul_right {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] (a b c : α) : gcd (b * a) (c * a) = gcd b c * normalize a

@[simp]

theorem gcd_mul_right' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b c : α) : Associated (gcd (b * a) (c * a)) (gcd b c * a)

theorem gcd_eq_left_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b

theorem gcd_eq_right_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) : gcd a b = b ↔ b ∣ a

theorem gcd_dvd_gcd_mul_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : gcd m n ∣ gcd (k * m) n

theorem gcd_dvd_gcd_mul_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : gcd m n ∣ gcd (m * k) n

theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : gcd m n ∣ gcd m (k * n)

theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : gcd m n ∣ gcd m (n * k)

theorem Associated.gcd_eq_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : gcd m k = gcd n k

theorem Associated.gcd_eq_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : gcd k m = gcd k n

theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ gcd k m * n

theorem dvd_gcd_mul_iff_dvd_mul {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {m n k : α} : k ∣ gcd k m * n ↔ k ∣ m * n

theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ m * gcd k n

theorem dvd_mul_gcd_iff_dvd_mul {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {m n k : α} : k ∣ m * gcd k n ↔ k ∣ m * n

instance instDecompositionMonoidOfIsGCDMonoid {α : Type u_1} [CommMonoidWithZero α] [h : IsGCDMonoid α] : DecompositionMonoid α

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 ℕ.

theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (k m n : α) : gcd k (m * n) ∣ gcd k m * gcd k n

theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} {k : ℕ} : gcd a (b ^ k) ∣ gcd a b ^ k

theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} {k : ℕ} : gcd (a ^ k) b ∣ gcd a b ^ k

theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [CommMonoidWithZero α] [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

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

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

theorem gcd_greatest {α : Type u_2} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) : gcd a b = normalize d

theorem gcd_greatest_associated {α : Type u_2} [CommMonoidWithZero α] [GCDMonoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) : Associated d (gcd a b)

theorem isUnit_gcd_of_eq_mul_gcd {α : Type u_2} [CommMonoidWithZero α] [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')

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

theorem associated_gcd_left_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {x y : α} : Associated x (gcd x y) ↔ x ∣ y

theorem associated_gcd_right_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {x y : α} : Associated y (gcd x y) ↔ y ∣ x

theorem Irreducible.isUnit_gcd_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {x y : α} (hx : Irreducible x) : IsUnit (gcd x y) ↔ ¬x ∣ y

theorem Irreducible.gcd_eq_one_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {x y : α} (hx : Irreducible x) : gcd x y = 1 ↔ ¬x ∣ y

theorem gcd_neg' {α : Type u_1} [CommMonoidWithZero α] [HasDistribNeg α] [GCDMonoid α] {a b : α} : Associated (gcd a (-b)) (gcd a b)

theorem gcd_neg {α : Type u_1} [CommMonoidWithZero α] [HasDistribNeg α] [NormalizedGCDMonoid α] {a b : α} : gcd a (-b) = gcd a b

theorem neg_gcd' {α : Type u_1} [CommMonoidWithZero α] [HasDistribNeg α] [GCDMonoid α] {a b : α} : Associated (gcd (-a) b) (gcd a b)

theorem neg_gcd {α : Type u_1} [CommMonoidWithZero α] [HasDistribNeg α] [NormalizedGCDMonoid α] {a b : α} : gcd (-a) b = gcd a b

theorem lcm_dvd_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

theorem dvd_lcm_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : a ∣ lcm a b

theorem dvd_lcm_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : b ∣ lcm a b

theorem lcm_dvd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b

@[simp]

theorem lcm_eq_zero_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0

theorem lcm_ne_zero_iff {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} : lcm a b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

@[simp]

theorem normalize_lcm {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b

theorem lcm_comm {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) : lcm a b = lcm b a

theorem lcm_comm' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (a b : α) : Associated (lcm a b) (lcm b a)

theorem lcm_assoc {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k)

theorem lcm_assoc' {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : Associated (lcm (lcm m n) k) (lcm m (lcm n k))

instance instCommutativeLcm {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] : Std.Commutative lcm

instance instAssociativeLcm {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] : Std.Associative lcm

theorem lcm_eq_normalize {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) : lcm a b = normalize c

theorem lcm_dvd_lcm {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣ lcm b d

theorem Associated.lcm {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) : Associated (lcm a₁ b₁) (lcm a₂ b₂)

@[simp]

theorem lcm_units_coe_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (u : αˣ) (a : α) : lcm (↑u) a = normalize a

@[simp]

theorem lcm_units_coe_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (u : αˣ) : lcm a ↑u = normalize a

@[simp]

theorem lcm_one_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : lcm 1 a = normalize a

@[simp]

theorem lcm_one_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : lcm a 1 = normalize a

@[simp]

theorem lcm_same {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) : lcm a a = normalize a

@[simp]

theorem lcm_eq_one_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) : lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1

@[simp]

theorem lcm_mul_left {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c

@[simp]

theorem lcm_mul_right {α : Type u_1} [CommMonoidWithZero α] [StrongNormalizedGCDMonoid α] (a b c : α) : lcm (b * a) (c * a) = lcm b c * normalize a

theorem lcm_eq_left_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a

theorem lcm_eq_right_iff {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b

theorem lcm_dvd_lcm_mul_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm (k * m) n

theorem lcm_dvd_lcm_mul_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm (m * k) n

theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm m (k * n)

theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n k : α) : lcm m n ∣ lcm m (n * k)

theorem lcm_eq_of_associated_left {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : lcm m k = lcm n k

theorem lcm_eq_of_associated_right {α : Type u_1} [CommMonoidWithZero α] [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : lcm k m = lcm k n

@[simp]

theorem lcm_dvd_mul {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] (m n : α) : lcm m n ∣ m * n

theorem dvd_lcm_of_dvd_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (h : a ∣ b) (c : α) : a ∣ lcm b c

theorem Dvd.dvd.lcm_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (h : a ∣ b) (c : α) : a ∣ lcm b c

Alias of dvd_lcm_of_dvd_left.

theorem dvd_of_lcm_right_dvd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c : α} (h : lcm a b ∣ c) : a ∣ c

theorem dvd_lcm_of_dvd_right {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (h : a ∣ b) (c : α) : a ∣ lcm c b

theorem Dvd.dvd.lcm_left {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} (h : a ∣ b) (c : α) : a ∣ lcm c b

Alias of dvd_lcm_of_dvd_right.

theorem dvd_of_lcm_left_dvd {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b c : α} (h : lcm a b ∣ c) : b ∣ c

theorem Prime.dvd_or_dvd_of_dvd_lcm {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b p : α} (hp : Prime p) (h : p ∣ lcm a b) : p ∣ a ∨ p ∣ b

theorem Prime.dvd_lcm {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b p : α} (hp : Prime p) : p ∣ lcm a b ↔ p ∣ a ∨ p ∣ b

theorem Prime.not_dvd_lcm {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b p : α} (hp : Prime p) (ha : ¬p ∣ a) (hb : ¬p ∣ b) : ¬p ∣ lcm a b

@[implicit_reducible, instance 100]

instance instStrongNormalizationMonoid {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : StrongNormalizationMonoid α

Equations

• instStrongNormalizationMonoid = { normUnit := fun (x : α) => 1, normUnit_zero := ⋯, normUnit_one := ⋯, normUnit_mul_units := ⋯, normUnit_mul := ⋯, normUnit_coe_units := ⋯ }

@[deprecated instStrongNormalizationMonoid (since := "2026-07-08")]

def NormalizationMonoid.ofUniqueUnits {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : StrongNormalizationMonoid α

Alias of instStrongNormalizationMonoid.

Equations

• @NormalizationMonoid.ofUniqueUnits = @instStrongNormalizationMonoid

@[implicit_reducible]

instance instUniqueNormalizationMonoid {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Unique (NormalizationMonoid α)

Equations

• instUniqueNormalizationMonoid = { default := inferInstance, uniq := ⋯ }

@[implicit_reducible]

instance instUniqueStrongNormalizationMonoid {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Unique (StrongNormalizationMonoid α)

Equations

• instUniqueStrongNormalizationMonoid = { default := inferInstance, uniq := ⋯ }

instance subsingleton_gcdMonoid_of_unique_units {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Subsingleton (GCDMonoid α)

instance subsingleton_normalizedGCDMonoid_of_unique_units {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Subsingleton (NormalizedGCDMonoid α)

instance instSubsingletonStrongNormalizedGCDMonoid {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Subsingleton (StrongNormalizedGCDMonoid α)

@[simp]

theorem normUnit_eq_one {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] (x : α) : normUnit x = 1

@[simp]

theorem normalize_eq {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] (x : α) : normalize x = x

def associatesEquivOfUniqueUnits {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] : Associates α ≃* α

If a monoid's only unit is 1, then it is isomorphic to its associates.

Equations

• associatesEquivOfUniqueUnits = { toFun := Associates.out, invFun := Associates.mk, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem associatesEquivOfUniqueUnits_symm_apply {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] (a : α) : associatesEquivOfUniqueUnits.symm a = Associates.mk a

@[simp]

theorem associatesEquivOfUniqueUnits_apply {α : Type u_1} [CommMonoidWithZero α] [Subsingleton αˣ] (a✝ : Associates α) : associatesEquivOfUniqueUnits a✝ = a✝.out

theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [CommRing α] [NormalizedGCDMonoid α] {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c

theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [CommRing α] [NormalizedGCDMonoid α] {a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a

@[implicit_reducible]

noncomputable def strongNormalizationMonoidOfMonoidHomRightInverse {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [DecidableEq α] (f : Associates α →* α) (hinv : Function.RightInverse (⇑f) Associates.mk) : StrongNormalizationMonoid α

Define NormalizationMonoid on a structure from a MonoidHom inverse to Associates.mk.

Equations

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

@[deprecated strongNormalizationMonoidOfMonoidHomRightInverse (since := "2026-07-08")]

def normalizationMonoidOfMonoidHomRightInverse {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [DecidableEq α] (f : Associates α →* α) (hinv : Function.RightInverse (⇑f) Associates.mk) : StrongNormalizationMonoid α

Alias of strongNormalizationMonoidOfMonoidHomRightInverse.

---

Define NormalizationMonoid on a structure from a MonoidHom inverse to Associates.mk.

Equations

• @normalizationMonoidOfMonoidHomRightInverse = @strongNormalizationMonoidOfMonoidHomRightInverse

@[implicit_reducible]

noncomputable def gcdMonoidOfGCD {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [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 α

Define GCDMonoid on a structure just from the gcd and its properties.

Equations

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

@[implicit_reducible]

noncomputable def normalizedGCDMonoidOfGCD {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [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 α

Define NormalizedGCDMonoid on a structure just from the gcd and its properties.

Equations

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

@[implicit_reducible]

noncomputable def gcdMonoidOfLCM {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [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 α

Define GCDMonoid on a structure just from the lcm and its properties.

Equations

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

@[implicit_reducible]

noncomputable def normalizedGCDMonoidOfLCM {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [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 α

Define NormalizedGCDMonoid on a structure just from the lcm and its properties.

Equations

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

@[implicit_reducible]

noncomputable def gcdMonoidOfExistsGCD {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) : GCDMonoid α

Define a GCDMonoid structure on a monoid just from the existence of a gcd.

Equations

• gcdMonoidOfExistsGCD h = gcdMonoidOfGCD (fun (a b : α) => Classical.choose ⋯) ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable def normalizedGCDMonoidOfExistsGCD {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [NormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) : NormalizedGCDMonoid α

Define a NormalizedGCDMonoid structure on a monoid just from the existence of a gcd.

Equations

• normalizedGCDMonoidOfExistsGCD h = normalizedGCDMonoidOfGCD (fun (a b : α) => normalize (Classical.choose ⋯)) ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

noncomputable abbrev strongNormalizedGCDMonoidOfExistsGCD {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [StrongNormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) : StrongNormalizedGCDMonoid α

Define a StrongNormalizedGCDMonoid structure on a monoid just from the existence of a gcd.

Equations

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

theorem nonempty_normalizedGCDMonoid_iff_isGCDMonoid {α : Type u_2} [CommMonoidWithZero α] : Nonempty (NormalizedGCDMonoid α) ↔ IsGCDMonoid α

instance instNonemptyNormalizedGCDMonoidOfIsGCDMonoid (α : Type u_2) [CommMonoidWithZero α] [IsGCDMonoid α] : Nonempty (NormalizedGCDMonoid α)

theorem nonempty_strongNormalizedGCDMonoid_iff {α : Type u_2} [CommMonoidWithZero α] : Nonempty (StrongNormalizedGCDMonoid α) ↔ IsGCDMonoid α ∧ Nonempty (StrongNormalizationMonoid α)

@[implicit_reducible]

noncomputable def gcdMonoidOfExistsLCM {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) : GCDMonoid α

Define a GCDMonoid structure on a monoid just from the existence of an lcm.

Equations

• gcdMonoidOfExistsLCM h = gcdMonoidOfLCM (fun (a b : α) => Classical.choose ⋯) ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable def normalizedGCDMonoidOfExistsLCM {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [NormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) : NormalizedGCDMonoid α

Define a NormalizedGCDMonoid structure on a monoid just from the existence of an lcm.

Equations

• normalizedGCDMonoidOfExistsLCM h = normalizedGCDMonoidOfLCM (fun (a b : α) => normalize (Classical.choose ⋯)) ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

noncomputable abbrev strongNormalizedGCDMonoidOfExistsLCM {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [StrongNormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) : StrongNormalizedGCDMonoid α

Define a StrongNormalizedGCDMonoid structure on a monoid just from the existence of a lcm.

Equations

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

theorem isGCDMonoid_iff_exists_gcd {α : Type u_2} [CommMonoidWithZero α] : IsGCDMonoid α ↔ IsCancelMulZero α ∧ ∀ (a b : α), ∃ (c : α), ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c

theorem isGCDMonoid_iff_exists_lcm {α : Type u_2} [CommMonoidWithZero α] : IsGCDMonoid α ↔ IsCancelMulZero α ∧ ∀ (a b : α), ∃ (c : α), ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d

@[implicit_reducible, instance 100]

instance CommGroupWithZero.instStrongNormalizedGCDMonoid (G₀ : Type u_2) [CommGroupWithZero G₀] [DecidableEq G₀] : StrongNormalizedGCDMonoid G₀

Equations

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

@[simp]

theorem CommGroupWithZero.coe_normUnit (G₀ : Type u_2) [CommGroupWithZero G₀] [DecidableEq G₀] {a : G₀} (h0 : a ≠ 0) : ↑(normUnit a) = a⁻¹

theorem CommGroupWithZero.normalize_eq_one (G₀ : Type u_2) [CommGroupWithZero G₀] [DecidableEq G₀] {a : G₀} (h0 : a ≠ 0) : normalize a = 1

@[implicit_reducible]

instance Associates.instGCDMonoid {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] : GCDMonoid (Associates α)

Equations

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

theorem Associates.gcd_mk_mk {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} : gcd (Associates.mk a) (Associates.mk b) = Associates.mk (gcd a b)

theorem Associates.lcm_mk_mk {α : Type u_1} [CommMonoidWithZero α] [GCDMonoid α] {a b : α} : lcm (Associates.mk a) (Associates.mk b) = Associates.mk (lcm a b)