Documentation

Mathlib.Algebra.GCDMonoid.Basic

Monoids with normalization functions, gcd, and lcm #

This file defines extra structures on CancelCommMonoidWithZeros, including IsDomains.

Main Definitions #

For the NormalizedGCDMonoid instances on and , see RingTheory.Int.Basic.

Implementation Notes #

TODO #

Tags #

divisibility, gcd, lcm, normalize

class NormalizationMonoid (α : Type u_1) [inst : CancelCommMonoidWithZero α] :
Type u_1
  • 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 0b 0normUnit (a * b) = normUnit a * normUnit b
  • The proposition that normUnit maps units to their inverses.

    normUnit_coe_units : ∀ (u : αˣ), normUnit u = u⁻¹

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

Instances
    @[simp]
    theorem normUnit_one {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] :
    def normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] :
    α →*₀ α

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem associated_normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (x : α) :
    Associated x (normalize x)
    theorem normalize_associated {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (x : α) :
    Associated (normalize x) x
    theorem associated_normalize_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {x : α} {y : α} :
    Associated x (normalize y) Associated x y
    theorem normalize_associated_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {x : α} {y : α} :
    Associated (normalize x) y Associated x y
    theorem Associates.mk_normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (x : α) :
    Associates.mk (normalize x) = Associates.mk x
    @[simp]
    theorem normalize_apply {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (x : α) :
    normalize x = x * ↑(normUnit x)
    theorem normalize_zero {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] :
    normalize 0 = 0
    theorem normalize_one {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] :
    normalize 1 = 1
    theorem normalize_coe_units {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (u : αˣ) :
    normalize u = 1
    theorem normalize_eq_zero {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {x : α} :
    normalize x = 0 x = 0
    theorem normalize_eq_one {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {x : α} :
    normalize x = 1 IsUnit x
    @[simp]
    theorem normUnit_mul_normUnit {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (a : α) :
    normUnit (a * ↑(normUnit a)) = 1
    theorem normalize_idem {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (x : α) :
    normalize (normalize x) = normalize x
    theorem normalize_eq_normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {a : α} {b : α} (hab : a b) (hba : b a) :
    normalize a = normalize b
    theorem normalize_eq_normalize_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {x : α} {y : α} :
    normalize x = normalize y x y y x
    theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {a : α} {b : α} (ha : normalize a = a) (hb : normalize b = b) (hab : a b) (hba : b a) :
    a = b
    theorem dvd_normalize_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {a : α} {b : α} :
    a normalize b a b
    theorem normalize_dvd_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] {a : α} {b : α} :
    normalize a b a b
    def Associates.out {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] :
    Associates αα

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

    Equations
    • Associates.out = Quotient.lift normalize (_ : ∀ (a x : α), a xnormalize a = normalize x)
    @[simp]
    theorem Associates.out_mk {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (a : α) :
    Associates.out (Associates.mk a) = normalize a
    @[simp]
    @[simp]
    theorem Associates.normalize_out {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] (a : Associates α) :
    normalize (Associates.out a) = Associates.out a
    @[simp]
    class GCDMonoid (α : Type u_1) [inst : CancelCommMonoidWithZero α] :
    Type u_1
    • 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
    • Tny common divisor of both elements is a divisor of the GCD.

      dvd_gcd : ∀ {a b c : α}, a ca ba 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: 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.

    Instances
      • 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: 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.

      Instances
        @[simp]
        theorem normalize_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) :
        normalize (gcd a b) = gcd a b
        theorem gcd_mul_lcm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        Associated (gcd a b * lcm a b) (a * b)
        theorem dvd_gcd_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) (c : α) :
        a gcd b c a b a c
        theorem gcd_comm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) :
        gcd a b = gcd b a
        theorem gcd_comm' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        Associated (gcd a b) (gcd b a)
        theorem gcd_assoc {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (m : α) (n : α) (k : α) :
        gcd (gcd m n) k = gcd m (gcd n k)
        theorem gcd_assoc' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        Associated (gcd (gcd m n) k) (gcd m (gcd n k))
        theorem gcd_eq_normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        gcd 0 a = normalize a
        theorem gcd_zero_left' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) :
        Associated (gcd 0 a) a
        @[simp]
        theorem gcd_zero_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        gcd a 0 = normalize a
        theorem gcd_zero_right' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) :
        Associated (gcd a 0) a
        @[simp]
        theorem gcd_eq_zero_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        gcd a b = 0 a = 0 b = 0
        @[simp]
        theorem gcd_one_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        gcd 1 a = 1
        @[simp]
        theorem gcd_one_left' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) :
        Associated (gcd 1 a) 1
        @[simp]
        theorem gcd_one_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        gcd a 1 = 1
        @[simp]
        theorem gcd_one_right' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) :
        Associated (gcd a 1) 1
        theorem gcd_dvd_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
        gcd a c gcd b d
        @[simp]
        theorem gcd_same {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        gcd a a = normalize a
        @[simp]
        theorem gcd_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :
        gcd (a * b) (a * c) = normalize a * gcd b c
        theorem gcd_mul_left' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) (c : α) :
        Associated (gcd (a * b) (a * c)) (a * gcd b c)
        @[simp]
        theorem gcd_mul_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :
        gcd (b * a) (c * a) = gcd b c * normalize a
        @[simp]
        theorem gcd_mul_right' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) (c : α) :
        Associated (gcd (b * a) (c * a)) (gcd b c * a)
        theorem gcd_eq_left_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (h : normalize a = a) :
        gcd a b = a a b
        theorem gcd_eq_right_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (h : normalize b = b) :
        gcd a b = b b a
        theorem gcd_dvd_gcd_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        gcd m n gcd (k * m) n
        theorem gcd_dvd_gcd_mul_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        gcd m n gcd (m * k) n
        theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        gcd m n gcd m (k * n)
        theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        gcd m n gcd m (n * k)
        theorem Associated.gcd_eq_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :
        gcd m k = gcd n k
        theorem Associated.gcd_eq_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :
        gcd k m = gcd k n
        theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {m : α} {n : α} {k : α} (H : k m * n) :
        k gcd k m * n
        theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {m : α} {n : α} {k : α} (H : k m * n) :
        k m * gcd k n
        theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {m : α} {n : α} {k : α} (H : k m * n) :
        d₁ d₂, d₁ m d₂ n k = d₁ * d₂

        Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

        In other words, the nonzero elements of a GCDMonoid form a decomposition monoid (more widely known as a pre-Schreier domain in the context of rings).

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

        See Nat.prodDvdAndDvdOfDvdProd for a constructive version on .

        theorem dvd_mul {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {k : α} {m : α} {n : α} :
        k m * n d₁ d₂, d₁ m d₂ n k = d₁ * d₂
        theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (k : α) (m : α) (n : α) :
        gcd k (m * n) gcd k m * gcd k n
        theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {k : } :
        gcd a (b ^ k) gcd a b ^ k
        theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {k : } :
        gcd (a ^ k) b gcd a b ^ k
        theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] [inst : Unique αˣ] {a : α} {b : α} {c : α} (hab : IsUnit (gcd a b)) {k : } (h : a * b = c ^ k) :
        d, a = d ^ k
        theorem gcd_greatest {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {a : α} {b : α} {d : α} (hda : d a) (hdb : d b) (hd : ∀ (e : α), e ae be d) :
        gcd a b = normalize d
        theorem gcd_greatest_associated {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {d : α} (hda : d a) (hdb : d b) (hd : ∀ (e : α), e ae be d) :
        Associated d (gcd a b)
        theorem isUnit_gcd_of_eq_mul_gcd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (x : α) (y : α) :
        x' y', x = gcd x y * x' y = gcd x y * y' IsUnit (gcd x' y')
        theorem lcm_dvd_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {c : α} :
        lcm a b c a c b c
        theorem dvd_lcm_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        a lcm a b
        theorem dvd_lcm_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        b lcm a b
        theorem lcm_dvd {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {c : α} (hab : a b) (hcb : c b) :
        lcm a c b
        @[simp]
        theorem lcm_eq_zero_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        lcm a b = 0 a = 0 b = 0
        @[simp]
        theorem normalize_lcm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) :
        normalize (lcm a b) = lcm a b
        theorem lcm_comm {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) :
        lcm a b = lcm b a
        theorem lcm_comm' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (a : α) (b : α) :
        Associated (lcm a b) (lcm b a)
        theorem lcm_assoc {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (m : α) (n : α) (k : α) :
        lcm (lcm m n) k = lcm m (lcm n k)
        theorem lcm_assoc' {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        Associated (lcm (lcm m n) k) (lcm m (lcm n k))
        theorem lcm_eq_normalize {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
        lcm a c lcm b d
        @[simp]
        theorem lcm_units_coe_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (u : αˣ) (a : α) :
        lcm (u) a = normalize a
        @[simp]
        theorem lcm_units_coe_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (u : αˣ) :
        lcm a u = normalize a
        @[simp]
        theorem lcm_one_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        lcm 1 a = normalize a
        @[simp]
        theorem lcm_one_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        lcm a 1 = normalize a
        @[simp]
        theorem lcm_same {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) :
        lcm a a = normalize a
        @[simp]
        theorem lcm_eq_one_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) :
        lcm a b = 1 a 1 b 1
        @[simp]
        theorem lcm_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :
        lcm (a * b) (a * c) = normalize a * lcm b c
        @[simp]
        theorem lcm_mul_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :
        lcm (b * a) (c * a) = lcm b c * normalize a
        theorem lcm_eq_left_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (h : normalize a = a) :
        lcm a b = a b a
        theorem lcm_eq_right_iff {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] (a : α) (b : α) (h : normalize b = b) :
        lcm a b = b a b
        theorem lcm_dvd_lcm_mul_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        lcm m n lcm (k * m) n
        theorem lcm_dvd_lcm_mul_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        lcm m n lcm (m * k) n
        theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        lcm m n lcm m (k * n)
        theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] (m : α) (n : α) (k : α) :
        lcm m n lcm m (n * k)
        theorem lcm_eq_of_associated_left {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :
        lcm m k = lcm n k
        theorem lcm_eq_of_associated_right {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :
        lcm k m = lcm k n
        theorem GCDMonoid.prime_of_irreducible {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : GCDMonoid α] {x : α} (hi : Irreducible x) :
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • uniqueNormalizationMonoidOfUniqueUnits = { toInhabited := { default := normalizationMonoidOfUniqueUnits }, uniq := (_ : ∀ (x : NormalizationMonoid α), x = default) }
        @[simp]
        theorem normUnit_eq_one {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : Unique αˣ] (x : α) :
        theorem normalize_eq {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : Unique αˣ] (x : α) :
        normalize x = x
        @[simp]
        theorem associatesEquivOfUniqueUnits_symm_apply {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : Unique αˣ] (a : α) :
        ↑(MulEquiv.symm associatesEquivOfUniqueUnits) a = Associates.mk a
        @[simp]
        theorem associatesEquivOfUniqueUnits_apply {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : Unique αˣ] :
        ∀ (a : Associates α), associatesEquivOfUniqueUnits a = Associates.out a

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

        Equations
        • One or more equations did not get rendered due to their size.
        theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [inst : CommRing α] [inst : IsDomain α] [inst : NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (h : a b - c) :
        gcd a b = gcd a c
        theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [inst : CommRing α] [inst : IsDomain α] [inst : NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (h : a b - c) :
        gcd b a = gcd c a
        def normalizationMonoidOfMonoidHomRightInverse {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : DecidableEq α] (f : Associates α →* α) (hinv : Function.RightInverse (f) Associates.mk) :

        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.
        noncomputable def gcdMonoidOfGCD {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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 ca ba gcd c b) :

        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.
        noncomputable def normalizedGCDMonoidOfGCD {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] [inst : 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 ca ba gcd c b) (normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b) :

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

        Equations
        noncomputable def gcdMonoidOfLCM {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : 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 ab alcm c b a) :

        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.
        noncomputable def normalizedGCDMonoidOfLCM {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] [inst : 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 ab alcm c b a) (normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b) :

        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.
        noncomputable def gcdMonoidOfExistsGCD {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : DecidableEq α] (h : ∀ (a b : α), c, ∀ (d : α), d a d b d c) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        noncomputable def normalizedGCDMonoidOfExistsGCD {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] [inst : DecidableEq α] (h : ∀ (a b : α), c, ∀ (d : α), d a d b d c) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        noncomputable def gcdMonoidOfExistsLCM {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : DecidableEq α] (h : ∀ (a b : α), c, ∀ (d : α), a d b d c d) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        noncomputable def normalizedGCDMonoidOfExistsLCM {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst : NormalizationMonoid α] [inst : DecidableEq α] (h : ∀ (a b : α), c, ∀ (d : α), a d b d c d) :

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

        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem CommGroupWithZero.coe_normUnit (G₀ : Type u_1) [inst : CommGroupWithZero G₀] [inst : DecidableEq G₀] {a : G₀} (h0 : a 0) :
        ↑(normUnit a) = a⁻¹
        theorem CommGroupWithZero.normalize_eq_one (G₀ : Type u_1) [inst : CommGroupWithZero G₀] [inst : DecidableEq G₀] {a : G₀} (h0 : a 0) :
        normalize a = 1