# mathlibdocumentation

algebra.gcd_monoid

# Monoids with normalization functions, gcd, and lcm#

This file defines extra structures on comm_cancel_monoid_with_zeros, including integral_domains.

## Main Definitions #

• normalization_monoid
• gcd_monoid
• gcd_monoid_of_exists_gcd
• gcd_monoid_of_exists_lcm

## Implementation Notes #

• normalization_monoid is defined by assigning to each element a norm_unit 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.

• gcd_monoid extends normalization_monoid, 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.

• gcd_monoid_of_gcd noncomputably constructs a gcd_monoid structure just from the gcd and its properties.

• gcd_monoid_of_exists_gcd noncomputably constructs a gcd_monoid structure just from a proof that any two elements have a (not necessarily normalized) gcd.

• gcd_monoid_of_lcm noncomputably constructs a gcd_monoid structure just from the lcm and its properties.

• gcd_monoid_of_exists_lcm noncomputably constructs a gcd_monoid structure just from a proof that any two elements have a (not necessarily normalized) lcm.

## TODO #

• Provide a GCD monoid instance for ℕ, port GCD facts about nats, definition of coprime
• Generalize normalization monoids to commutative (cancellative) monoids with or without zero
• Generalize GCD monoid to not require normalization in all cases

## Tags #

divisibility, gcd, lcm, normalize

@[class]
structure normalization_monoid (α : Type u_2) [nontrivial α]  :
Type u_2
• norm_unit : α →
• norm_unit_zero : = 1
• norm_unit_mul : ∀ {a b : α}, a 0b 0norm_unit (a * b) = (norm_unit a) *
• norm_unit_coe_units : ∀ (u : units α),

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

Instances
@[simp]
theorem norm_unit_one {α : Type u_1} [nontrivial α]  :
= 1
def normalize {α : Type u_1} [nontrivial α]  :

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

Equations
theorem associated_normalize {α : Type u_1} [nontrivial α] {x : α} :
theorem normalize_associated {α : Type u_1} [nontrivial α] {x : α} :
x
theorem associates.mk_normalize {α : Type u_1} [nontrivial α] {x : α} :
@[simp]
theorem normalize_apply {α : Type u_1} [nontrivial α] {x : α} :
@[simp]
theorem normalize_zero {α : Type u_1} [nontrivial α]  :
= 0
@[simp]
theorem normalize_one {α : Type u_1} [nontrivial α]  :
= 1
theorem normalize_coe_units {α : Type u_1} [nontrivial α] (u : units α) :
= 1
theorem normalize_eq_zero {α : Type u_1} [nontrivial α] {x : α} :
= 0 x = 0
theorem normalize_eq_one {α : Type u_1} [nontrivial α] {x : α} :
= 1
@[simp]
theorem norm_unit_mul_norm_unit {α : Type u_1} [nontrivial α] (a : α) :
theorem normalize_idem {α : Type u_1} [nontrivial α] (x : α) :
theorem normalize_eq_normalize {α : Type u_1} [nontrivial α] {a b : α} (hab : a b) (hba : b a) :
theorem normalize_eq_normalize_iff {α : Type u_1} [nontrivial α] {x y : α} :
x y y x
theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [nontrivial α] {a b : α} (ha : = a) (hb : = b) (hab : a b) (hba : b a) :
a = b
theorem dvd_normalize_iff {α : Type u_1} [nontrivial α] {a b : α} :
a a b
theorem normalize_dvd_iff {α : Type u_1} [nontrivial α] {a b : α} :
b a b
@[instance]
Equations
@[simp]
theorem comm_group_with_zero.coe_norm_unit {α : Type u_1} [decidable_eq α] {a : α} (h0 : a 0) :
def associates.out {α : Type u_1} [nontrivial α]  :
→ α

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

Equations
theorem associates.out_mk {α : Type u_1} [nontrivial α] (a : α) :
.out =
@[simp]
theorem associates.out_one {α : Type u_1} [nontrivial α]  :
1.out = 1
theorem associates.out_mul {α : Type u_1} [nontrivial α] (a b : associates α) :
(a * b).out = (a.out) * b.out
theorem associates.dvd_out_iff {α : Type u_1} [nontrivial α] (a : α) (b : associates α) :
a b.out
theorem associates.out_dvd_iff {α : Type u_1} [nontrivial α] (a : α) (b : associates α) :
b.out a
@[simp]
theorem associates.out_top {α : Type u_1} [nontrivial α]  :
@[simp]
theorem associates.normalize_out {α : Type u_1} [nontrivial α] (a : associates α) :
= a.out
@[class]
structure gcd_monoid (α : Type u_2) [nontrivial α] :
Type u_2
• norm_unit : α →
• norm_unit_zero :
• norm_unit_mul : ∀ {a b : α}, a 0b 0
• norm_unit_coe_units : ∀ (u : units α),
• 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_1 : α}, a c_1a ba gcd c_1 b
• normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
• gcd_mul_lcm : ∀ (a b : α), (gcd a b) * lcm a b = normalize (a * b)
• lcm_zero_left : ∀ (a : α), lcm 0 a = 0
• lcm_zero_right : ∀ (a : α), lcm a 0 = 0

GCD monoid: a comm_cancel_monoid_with_zero 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
@[instance]
def gcd_monoid.to_normalization_monoid (α : Type u_2) [nontrivial α] [self : gcd_monoid α] :
@[simp]
theorem normalize_gcd {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
normalize (gcd a b) = gcd a b
@[simp]
theorem gcd_mul_lcm {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
(gcd a b) * lcm a b = normalize (a * b)
theorem dvd_gcd_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b c : α) :
a gcd b c a b a c
theorem gcd_comm {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
gcd a b = gcd b a
theorem gcd_assoc {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd (gcd m n) k = gcd m (gcd n k)
@[instance]
def gcd_monoid.gcd.is_commutative {α : Type u_1} [nontrivial α] [gcd_monoid α] :
@[instance]
def gcd_monoid.gcd.is_associative {α : Type u_1} [nontrivial α] [gcd_monoid α] :
theorem gcd_eq_normalize {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c : α} (habc : gcd a b c) (hcab : c gcd a b) :
gcd a b =
@[simp]
theorem gcd_zero_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
gcd 0 a =
@[simp]
theorem gcd_zero_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
gcd a 0 =
@[simp]
theorem gcd_eq_zero_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
gcd a b = 0 a = 0 b = 0
@[simp]
theorem gcd_one_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
gcd 1 a = 1
@[simp]
theorem gcd_one_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
gcd a 1 = 1
theorem gcd_dvd_gcd {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c d : α} (hab : a b) (hcd : c d) :
gcd a c gcd b d
@[simp]
theorem gcd_same {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
gcd a a =
@[simp]
theorem gcd_mul_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b c : α) :
gcd (a * b) (a * c) = (normalize a) * gcd b c
@[simp]
theorem gcd_mul_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b c : α) :
gcd (b * a) (c * a) = (gcd b c) *
theorem gcd_eq_left_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) (h : = a) :
gcd a b = a a b
theorem gcd_eq_right_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) (h : = b) :
gcd a b = b b a
theorem gcd_dvd_gcd_mul_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd (k * m) n
theorem gcd_dvd_gcd_mul_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd (m * k) n
theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd m (k * n)
theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd m (n * k)
theorem gcd_eq_of_associated_left {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n : α} (h : n) (k : α) :
gcd m k = gcd n k
theorem gcd_eq_of_associated_right {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n : α} (h : n) (k : α) :
gcd k m = gcd k n
theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n k : α} (H : k m * n) :
k (gcd k m) * n
theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n k : α} (H : k m * n) :
k m * gcd k n
theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n k : α} (H : k m * n) :
∃ (d₁ : α) (hd₁ : d₁ m) (d₂ : α) (hd₂ : d₂ n), k = d₁ * d₂

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.

theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [nontrivial α] [gcd_monoid α] (k m n : α) :
gcd k (m * n) (gcd k m) * gcd k n
theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b : α} {k : } :
gcd a (b ^ k) gcd a b ^ k
theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b : α} {k : } :
gcd (a ^ k) b gcd a b ^ k
theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c d₁ d₂ : α} (ha : a 0) (hab : gcd a b = 1) {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} [nontrivial α] [gcd_monoid α] {a b c : α} (hab : gcd a b = 1) {k : } (h : a * b = c ^ k) :
∃ (d : α), associated (d ^ k) a
theorem lcm_dvd_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c : α} :
lcm a b c a c b c
theorem dvd_lcm_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
a lcm a b
theorem dvd_lcm_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
b lcm a b
theorem lcm_dvd {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c : α} (hab : a b) (hcb : c b) :
lcm a c b
@[simp]
theorem lcm_eq_zero_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = 0 a = 0 b = 0
@[simp]
theorem normalize_lcm {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
normalize (lcm a b) = lcm a b
theorem lcm_comm {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = lcm b a
theorem lcm_assoc {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm (lcm m n) k = lcm m (lcm n k)
@[instance]
def gcd_monoid.lcm.is_commutative {α : Type u_1} [nontrivial α] [gcd_monoid α] :
@[instance]
def gcd_monoid.lcm.is_associative {α : Type u_1} [nontrivial α] [gcd_monoid α] :
theorem lcm_eq_normalize {α : Type u_1} [nontrivial α] [gcd_monoid α] {a b c : α} (habc : lcm a b c) (hcab : c lcm a b) :
lcm a b =
theorem lcm_dvd_lcm {α : Type u_1} [nontrivial α] [gcd_monoid α] {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} [nontrivial α] [gcd_monoid α] (u : units α) (a : α) :
lcm u a =
@[simp]
theorem lcm_units_coe_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) (u : units α) :
lcm a u =
@[simp]
theorem lcm_one_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
lcm 1 a =
@[simp]
theorem lcm_one_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
lcm a 1 =
@[simp]
theorem lcm_same {α : Type u_1} [nontrivial α] [gcd_monoid α] (a : α) :
lcm a a =
@[simp]
theorem lcm_eq_one_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = 1 a 1 b 1
@[simp]
theorem lcm_mul_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b c : α) :
lcm (a * b) (a * c) = (normalize a) * lcm b c
@[simp]
theorem lcm_mul_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b c : α) :
lcm (b * a) (c * a) = (lcm b c) *
theorem lcm_eq_left_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) (h : = a) :
lcm a b = a b a
theorem lcm_eq_right_iff {α : Type u_1} [nontrivial α] [gcd_monoid α] (a b : α) (h : = b) :
lcm a b = b a b
theorem lcm_dvd_lcm_mul_left {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm (k * m) n
theorem lcm_dvd_lcm_mul_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm (m * k) n
theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm m (k * n)
theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm m (n * k)
theorem lcm_eq_of_associated_left {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n : α} (h : n) (k : α) :
lcm m k = lcm n k
theorem lcm_eq_of_associated_right {α : Type u_1} [nontrivial α] [gcd_monoid α] {m n : α} (h : n) (k : α) :
lcm k m = lcm k n
theorem gcd_monoid.prime_of_irreducible {α : Type u_1} [nontrivial α] [gcd_monoid α] {x : α} (hi : irreducible x) :
theorem gcd_monoid.irreducible_iff_prime {α : Type u_1} [nontrivial α] [gcd_monoid α] {p : α} :
theorem units_eq_one {α : Type u_1} [unique (units α)] (u : units α) :
u = 1
@[instance]
def normalization_monoid_of_unique_units {α : Type u_1} [unique (units α)] [nontrivial α] :
Equations
@[simp]
theorem norm_unit_eq_one {α : Type u_1} [unique (units α)] [nontrivial α] (x : α) :
= 1
@[simp]
theorem normalize_eq {α : Type u_1} [unique (units α)] [nontrivial α] (x : α) :
= x
theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [gcd_monoid α] {a b c : α} (h : a b - c) :
gcd a b = gcd a c
theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [gcd_monoid α] {a b c : α} (h : a b - c) :
gcd b a = gcd c a

Define normalization_monoid on a structure from a monoid_hom inverse to associates.mk.

Equations
def gcd_monoid_of_gcd {α : Type u_1} [nontrivial α] [decidable_eq α] (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 gcd_monoid on a structure just from the gcd and its properties.

Equations
def gcd_monoid_of_lcm {α : Type u_1} [nontrivial α] [decidable_eq α] (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 gcd_monoid on a structure just from the lcm and its properties.

Equations
def gcd_monoid_of_exists_gcd {α : Type u_1} [nontrivial α] [decidable_eq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), d a d b d c) :

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

Equations
def gcd_monoid_of_exists_lcm {α : Type u_1} [nontrivial α] [decidable_eq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), a d b d c d) :

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

Equations
@[instance]

ℕ is a gcd_monoid

Equations
@[simp]
theorem nat.normalize_eq (n : ) :
= n
theorem nat.gcd_eq_gcd (m n : ) :
gcd m n = m.gcd n
theorem nat.lcm_eq_lcm (m n : ) :
lcm m n = m.lcm n