# Monoids with normalization functions, gcd, and lcm#

This file defines extra structures on CancelCommMonoidWithZeros, including IsDomains.

## Main Definitions #

• NormalizationMonoid
• GCDMonoid
• NormalizedGCDMonoid
• gcdMonoid_of_gcd, gcdMonoid_of_exists_gcd, normalizedGCDMonoid_of_gcd, normalizedGCDMonoid_of_exists_gcd
• gcdMonoid_of_lcm, gcdMonoid_of_exists_lcm, normalizedGCDMonoid_of_lcm, normalizedGCDMonoid_of_exists_lcm

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

## 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 monoid homomorphism. This definition as currently implemented does casework on 0.

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

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

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

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

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

• gcdMonoid_of_exists_lcm and normalizedGCDMonoid_of_exists_lcm 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) :
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 : = 1

The proposition that normUnit maps 0 to the identity.

• normUnit_mul : ∀ {a b : α}, a 0b 0normUnit (a * 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.

Instances
@[simp]
theorem normUnit_one {α : Type u_1} :
= 1
def normalize {α : Type u_1} :
α →*₀ α

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

Equations
• normalize = { toZeroHom := { toFun := fun (x : α) => x * (), map_zero' := }, map_one' := , map_mul' := }
Instances For
theorem associated_normalize {α : Type u_1} (x : α) :
Associated x (normalize x)
theorem normalize_associated {α : Type u_1} (x : α) :
Associated (normalize x) x
theorem associated_normalize_iff {α : Type u_1} {x : α} {y : α} :
Associated x (normalize y)
theorem normalize_associated_iff {α : Type u_1} {x : α} {y : α} :
Associated (normalize x) y
theorem Associates.mk_normalize {α : Type u_1} (x : α) :
Associates.mk (normalize x) =
@[simp]
theorem normalize_apply {α : Type u_1} (x : α) :
normalize x = x * ()
theorem normalize_zero {α : Type u_1} :
normalize 0 = 0
theorem normalize_one {α : Type u_1} :
normalize 1 = 1
theorem normalize_coe_units {α : Type u_1} (u : αˣ) :
normalize u = 1
theorem normalize_eq_zero {α : Type u_1} {x : α} :
normalize x = 0 x = 0
theorem normalize_eq_one {α : Type u_1} {x : α} :
normalize x = 1
@[simp]
theorem normUnit_mul_normUnit {α : Type u_1} (a : α) :
normUnit (a * ()) = 1
theorem normalize_idem {α : Type u_1} (x : α) :
normalize (normalize x) = normalize x
theorem normalize_eq_normalize {α : Type u_1} {a : α} {b : α} (hab : a b) (hba : b a) :
normalize a = normalize b
theorem normalize_eq_normalize_iff {α : Type u_1} {x : α} {y : α} :
normalize x = normalize y x y y x
theorem dvd_antisymm_of_normalize_eq {α : Type u_1} {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} {a : α} {b : α} :
a normalize b a b
theorem normalize_dvd_iff {α : Type u_1} {a : α} {b : α} :
normalize a b a b
def Associates.out {α : Type u_1} :
α

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

Equations
Instances For
@[simp]
theorem Associates.out_mk {α : Type u_1} (a : α) :
= normalize a
@[simp]
theorem Associates.out_one {α : Type u_1} :
theorem Associates.out_mul {α : Type u_1} (a : ) (b : ) :
theorem Associates.dvd_out_iff {α : Type u_1} (a : α) (b : ) :
theorem Associates.out_dvd_iff {α : Type u_1} (a : α) (b : ) :
@[simp]
theorem Associates.out_top {α : Type u_1} :
@[simp]
theorem Associates.normalize_out {α : Type u_1} (a : ) :
normalize () =
@[simp]
theorem Associates.mk_out {α : Type u_1} (a : ) :
theorem Associates.out_injective {α : Type u_1} :
Function.Injective Associates.out
class GCDMonoid (α : Type u_2) :
Type u_2

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.

• 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 ca ba 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.

Instances
class NormalizedGCDMonoid (α : Type u_2) extends , :
Type u_2

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.

• normUnit : ααˣ
• normUnit_zero : = 1
• normUnit_mul : ∀ {a b : α}, a 0b 0normUnit (a * b) =
• normUnit_coe_units : ∀ (u : αˣ), normUnit u = u⁻¹
• 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 ca ba 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.

Instances
Equations
• =
instance instNonemptyGCDMonoid {α : Type u_1} [] :
Equations
• =
Equations
• =
instance instNonemptyNormalizationMonoid_1 {α : Type u_1} [h : ] :
Equations
• =
instance instNonemptyGCDMonoid_1 {α : Type u_1} [h : ] :
Equations
• =
theorem gcd_isUnit_iff_isRelPrime {α : Type u_1} [] {a : α} {b : α} :
IsUnit (gcd a b)
@[simp]
theorem normalize_gcd {α : Type u_1} (a : α) (b : α) :
normalize (gcd a b) = gcd a b
theorem gcd_mul_lcm {α : Type u_1} [] (a : α) (b : α) :
Associated (gcd a b * lcm a b) (a * b)
theorem dvd_gcd_iff {α : Type u_1} [] (a : α) (b : α) (c : α) :
a gcd b c a b a c
theorem gcd_comm {α : Type u_1} (a : α) (b : α) :
gcd a b = gcd b a
theorem gcd_comm' {α : Type u_1} [] (a : α) (b : α) :
Associated (gcd a b) (gcd b a)
theorem gcd_assoc {α : Type u_1} (m : α) (n : α) (k : α) :
gcd (gcd m n) k = gcd m (gcd n k)
theorem gcd_assoc' {α : Type u_1} [] (m : α) (n : α) (k : α) :
Associated (gcd (gcd m n) k) (gcd m (gcd n k))
instance instCommutativeGcdToGCDMonoid {α : Type u_1} :
Equations
• =
instance instAssociativeGcdToGCDMonoid {α : Type u_1} :
Equations
• =
theorem gcd_eq_normalize {α : Type u_1} {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} (a : α) :
gcd 0 a = normalize a
theorem gcd_zero_left' {α : Type u_1} [] (a : α) :
Associated (gcd 0 a) a
@[simp]
theorem gcd_zero_right {α : Type u_1} (a : α) :
gcd a 0 = normalize a
theorem gcd_zero_right' {α : Type u_1} [] (a : α) :
Associated (gcd a 0) a
@[simp]
theorem gcd_eq_zero_iff {α : Type u_1} [] (a : α) (b : α) :
gcd a b = 0 a = 0 b = 0
@[simp]
theorem gcd_one_left {α : Type u_1} (a : α) :
gcd 1 a = 1
@[simp]
theorem isUnit_gcd_one_left {α : Type u_1} [] (a : α) :
IsUnit (gcd 1 a)
theorem gcd_one_left' {α : Type u_1} [] (a : α) :
Associated (gcd 1 a) 1
@[simp]
theorem gcd_one_right {α : Type u_1} (a : α) :
gcd a 1 = 1
@[simp]
theorem isUnit_gcd_one_right {α : Type u_1} [] (a : α) :
IsUnit (gcd a 1)
theorem gcd_one_right' {α : Type u_1} [] (a : α) :
Associated (gcd a 1) 1
theorem gcd_dvd_gcd {α : Type u_1} [] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
gcd a c gcd b d
@[simp]
theorem gcd_same {α : Type u_1} (a : α) :
gcd a a = normalize a
@[simp]
theorem gcd_mul_left {α : Type u_1} (a : α) (b : α) (c : α) :
gcd (a * b) (a * c) = normalize a * gcd b c
theorem gcd_mul_left' {α : Type u_1} [] (a : α) (b : α) (c : α) :
Associated (gcd (a * b) (a * c)) (a * gcd b c)
@[simp]
theorem gcd_mul_right {α : Type u_1} (a : α) (b : α) (c : α) :
gcd (b * a) (c * a) = gcd b c * normalize a
@[simp]
theorem gcd_mul_right' {α : Type u_1} [] (a : α) (b : α) (c : α) :
Associated (gcd (b * a) (c * a)) (gcd b c * a)
theorem gcd_eq_left_iff {α : Type u_1} (a : α) (b : α) (h : normalize a = a) :
gcd a b = a a b
theorem gcd_eq_right_iff {α : Type u_1} (a : α) (b : α) (h : normalize b = b) :
gcd a b = b b a
theorem gcd_dvd_gcd_mul_left {α : Type u_1} [] (m : α) (n : α) (k : α) :
gcd m n gcd (k * m) n
theorem gcd_dvd_gcd_mul_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
gcd m n gcd (m * k) n
theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
gcd m n gcd m (k * n)
theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
gcd m n gcd m (n * k)
theorem Associated.gcd_eq_left {α : Type u_1} {m : α} {n : α} (h : ) (k : α) :
gcd m k = gcd n k
theorem Associated.gcd_eq_right {α : Type u_1} {m : α} {n : α} (h : ) (k : α) :
gcd k m = gcd k n
theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [] {m : α} {n : α} {k : α} (H : k m * n) :
k gcd k m * n
theorem dvd_gcd_mul_iff_dvd_mul {α : Type u_1} [] {m : α} {n : α} {k : α} :
k gcd k m * n k m * n
theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [] {m : α} {n : α} {k : α} (H : k m * n) :
k m * gcd k n
theorem dvd_mul_gcd_iff_dvd_mul {α : Type u_1} [] {m : α} {n : α} {k : α} :
k m * gcd k n k m * n

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.prodDvdAndDvdOfDvdProd for a constructive version on .

Equations
• =
theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [] (k : α) (m : α) (n : α) :
gcd k (m * n) gcd k m * gcd k n
theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [] {a : α} {b : α} {k : } :
gcd a (b ^ k) gcd a b ^ k
theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [] {a : α} {b : α} {k : } :
gcd (a ^ k) b gcd a b ^ k
theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [] {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} [] {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} [] [] {a : α} {b : α} {c : α} (hab : IsUnit (gcd a b)) {k : } (h : a * b = c ^ k) :
∃ (d : α), a = d ^ k
theorem gcd_greatest {α : Type u_2} {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_2} [] {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_2} [] {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} [] (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} [] {x : α} {y : α} :
Associated x (gcd x y) x y
theorem associated_gcd_right_iff {α : Type u_1} [] {x : α} {y : α} :
Associated y (gcd x y) y x
theorem Irreducible.isUnit_gcd_iff {α : Type u_1} [] {x : α} {y : α} (hx : ) :
IsUnit (gcd x y) ¬x y
theorem Irreducible.gcd_eq_one_iff {α : Type u_1} {x : α} {y : α} (hx : ) :
gcd x y = 1 ¬x y
theorem lcm_dvd_iff {α : Type u_1} [] {a : α} {b : α} {c : α} :
lcm a b c a c b c
theorem dvd_lcm_left {α : Type u_1} [] (a : α) (b : α) :
a lcm a b
theorem dvd_lcm_right {α : Type u_1} [] (a : α) (b : α) :
b lcm a b
theorem lcm_dvd {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a b) (hcb : c b) :
lcm a c b
@[simp]
theorem lcm_eq_zero_iff {α : Type u_1} [] (a : α) (b : α) :
lcm a b = 0 a = 0 b = 0
@[simp]
theorem normalize_lcm {α : Type u_1} (a : α) (b : α) :
normalize (lcm a b) = lcm a b
theorem lcm_comm {α : Type u_1} (a : α) (b : α) :
lcm a b = lcm b a
theorem lcm_comm' {α : Type u_1} [] (a : α) (b : α) :
Associated (lcm a b) (lcm b a)
theorem lcm_assoc {α : Type u_1} (m : α) (n : α) (k : α) :
lcm (lcm m n) k = lcm m (lcm n k)
theorem lcm_assoc' {α : Type u_1} [] (m : α) (n : α) (k : α) :
Associated (lcm (lcm m n) k) (lcm m (lcm n k))
instance instCommutativeLcmToGCDMonoid {α : Type u_1} :
Equations
• =
instance instAssociativeLcmToGCDMonoid {α : Type u_1} :
Equations
• =
theorem lcm_eq_normalize {α : Type u_1} {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} [] {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} (u : αˣ) (a : α) :
lcm (u) a = normalize a
@[simp]
theorem lcm_units_coe_right {α : Type u_1} (a : α) (u : αˣ) :
lcm a u = normalize a
@[simp]
theorem lcm_one_left {α : Type u_1} (a : α) :
lcm 1 a = normalize a
@[simp]
theorem lcm_one_right {α : Type u_1} (a : α) :
lcm a 1 = normalize a
@[simp]
theorem lcm_same {α : Type u_1} (a : α) :
lcm a a = normalize a
@[simp]
theorem lcm_eq_one_iff {α : Type u_1} (a : α) (b : α) :
lcm a b = 1 a 1 b 1
@[simp]
theorem lcm_mul_left {α : Type u_1} (a : α) (b : α) (c : α) :
lcm (a * b) (a * c) = normalize a * lcm b c
@[simp]
theorem lcm_mul_right {α : Type u_1} (a : α) (b : α) (c : α) :
lcm (b * a) (c * a) = lcm b c * normalize a
theorem lcm_eq_left_iff {α : Type u_1} (a : α) (b : α) (h : normalize a = a) :
lcm a b = a b a
theorem lcm_eq_right_iff {α : Type u_1} (a : α) (b : α) (h : normalize b = b) :
lcm a b = b a b
theorem lcm_dvd_lcm_mul_left {α : Type u_1} [] (m : α) (n : α) (k : α) :
lcm m n lcm (k * m) n
theorem lcm_dvd_lcm_mul_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
lcm m n lcm (m * k) n
theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
lcm m n lcm m (k * n)
theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [] (m : α) (n : α) (k : α) :
lcm m n lcm m (n * k)
theorem lcm_eq_of_associated_left {α : Type u_1} {m : α} {n : α} (h : ) (k : α) :
lcm m k = lcm n k
theorem lcm_eq_of_associated_right {α : Type u_1} {m : α} {n : α} (h : ) (k : α) :
lcm k m = lcm k n
@[deprecated Irreducible.prime]
theorem GCDMonoid.prime_of_irreducible {α : Type u_1} {a : α} (irr : ) :

Alias of Irreducible.prime.

@[deprecated irreducible_iff_prime]
theorem GCDMonoid.irreducible_iff_prime {α : Type u_1} {a : α} :

Alias of irreducible_iff_prime.

instance normalizationMonoidOfUniqueUnits {α : Type u_1} [] :
Equations
• normalizationMonoidOfUniqueUnits = { normUnit := fun (x : α) => 1, normUnit_zero := , normUnit_mul := , normUnit_coe_units := }
Equations
• uniqueNormalizationMonoidOfUniqueUnits = { toInhabited := { default := normalizationMonoidOfUniqueUnits }, uniq := }
Equations
• =
Equations
• =
@[simp]
theorem normUnit_eq_one {α : Type u_1} [] (x : α) :
= 1
theorem normalize_eq {α : Type u_1} [] (x : α) :
normalize x = x
@[simp]
theorem associatesEquivOfUniqueUnits_symm_apply {α : Type u_1} [] (a : α) :
(MulEquiv.symm associatesEquivOfUniqueUnits) a =
@[simp]
theorem associatesEquivOfUniqueUnits_apply {α : Type u_1} [] :
∀ (a : ), associatesEquivOfUniqueUnits a =
def associatesEquivOfUniqueUnits {α : Type u_1} [] :
≃* α

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

Equations
• associatesEquivOfUniqueUnits = { toEquiv := { toFun := Associates.out, invFun := Associates.mk, left_inv := , right_inv := }, map_mul' := }
Instances For
theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : a b - c) :
gcd a b = gcd a c
theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [] [] {a : α} {b : α} {c : α} (h : a b - c) :
gcd b a = gcd c a
def normalizationMonoidOfMonoidHomRightInverse {α : Type u_1} [] (f : →* α) (hinv : Function.RightInverse (f) Associates.mk) :

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

Equations
• = { normUnit := fun (a : α) => if a = 0 then 1 else , normUnit_zero := , normUnit_mul := , normUnit_coe_units := }
Instances For
noncomputable def gcdMonoidOfGCD {α : Type u_1} [] (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.
Instances For
noncomputable def normalizedGCDMonoidOfGCD {α : Type u_1} [] (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
Instances For
noncomputable def gcdMonoidOfLCM {α : Type u_1} [] (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.
Instances For
noncomputable def normalizedGCDMonoidOfLCM {α : Type u_1} [] (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
Instances For
noncomputable def gcdMonoidOfExistsGCD {α : Type u_1} [] (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
Instances For
noncomputable def normalizedGCDMonoidOfExistsGCD {α : Type u_1} [] (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
Instances For
noncomputable def gcdMonoidOfExistsLCM {α : Type u_1} [] (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
Instances For
noncomputable def normalizedGCDMonoidOfExistsLCM {α : Type u_1} [] (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
Instances For
@[simp]
theorem CommGroupWithZero.coe_normUnit (G₀ : Type u_2) [] [] {a : G₀} (h0 : a 0) :
() = a⁻¹
theorem CommGroupWithZero.normalize_eq_one (G₀ : Type u_2) [] [] {a : G₀} (h0 : a 0) :
normalize a = 1
theorem Associated.gcd {α : Type u_1} [] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
Associated (gcd a₁ b₁) (gcd a₂ b₂)
theorem Associated.lcm {α : Type u_1} [] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
Associated (lcm a₁ b₁) (lcm a₂ b₂)
instance Associates.instGCDMonoid {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem Associates.gcd_mk_mk {α : Type u_1} [] {a : α} {b : α} :
gcd () () = Associates.mk (gcd a b)
theorem Associates.lcm_mk_mk {α : Type u_1} [] {a : α} {b : α} :
lcm () () = Associates.mk (lcm a b)