mathlib documentation

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

Implementation Notes

TODO

Tags

divisibility, gcd, lcm, normalize

@[class]
structure normalization_monoid (α : Type u_2) [nontrivial α] [comm_cancel_monoid_with_zero α] :
Type u_2

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

Instances
@[simp]

def normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] :
α →* α

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

Equations
@[simp]
theorem normalize_apply {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {x : α} :

@[simp]

@[simp]

theorem normalize_eq_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {x : α} :

@[simp]
theorem norm_unit_mul_norm_unit {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : α) :

theorem normalize_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} :
a bb anormalize a = normalize b

theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} :
normalize a = anormalize b = ba bb aa = b

theorem dvd_normalize_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} :

theorem normalize_dvd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} :

@[instance]

Equations
@[simp]
theorem comm_group_with_zero.coe_norm_unit {α : Type u_1} [decidable_eq α] [comm_group_with_zero α] {a : α} :
a 0(norm_unit a) = a⁻¹

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

Equations
@[simp]

theorem associates.out_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a b : associates α) :
(a * b).out = (a.out) * b.out

@[simp]

@[class]
structure gcd_monoid (α : Type u_2) [comm_cancel_monoid_with_zero α] [nontrivial α] :
Type u_2

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
@[simp]
theorem normalize_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize (gcd a b) = gcd a b

@[simp]
theorem gcd_mul_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
(gcd a b) * lcm a b = normalize (a * b)

theorem dvd_gcd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b c : α) :
a gcd b c a b a c

theorem gcd_comm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
gcd a b = gcd b a

theorem gcd_assoc {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd (gcd m n) k = gcd m (gcd n k)

theorem gcd_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} :
gcd a b cc gcd a bgcd a b = normalize c

@[simp]
theorem gcd_zero_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem gcd_zero_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem gcd_eq_zero_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
gcd a b = 0 a = 0 b = 0

@[simp]
theorem gcd_one_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :
gcd 1 a = 1

@[simp]
theorem gcd_one_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :
gcd a 1 = 1

theorem gcd_dvd_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c d : α} :
a bc dgcd a c gcd b d

@[simp]
theorem gcd_same {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem gcd_mul_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b c : α) :
gcd (a * b) (a * c) = (normalize a) * gcd b c

@[simp]
theorem gcd_mul_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b c : α) :
gcd (b * a) (c * a) = (gcd b c) * normalize a

theorem gcd_eq_left_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize a = a(gcd a b = a a b)

theorem gcd_eq_right_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize b = b(gcd a b = b b a)

theorem gcd_dvd_gcd_mul_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd (k * m) n

theorem gcd_dvd_gcd_mul_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd (m * k) n

theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd m (k * n)

theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
gcd m n gcd m (n * k)

theorem gcd_eq_of_associated_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
gcd m k = gcd n k

theorem gcd_eq_of_associated_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
gcd k m = gcd k n

theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n k : α} :
k m * nk (gcd k m) * n

theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n k : α} :
k m * nk m * gcd k n

theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n k : α} :
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} [comm_cancel_monoid_with_zero α] [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} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b : α} {k : } :
gcd a (b ^ k) gcd a b ^ k

theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b : α} {k : } :
gcd (a ^ k) b gcd a b ^ k

theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c d₁ d₂ : α} (ha : a 0) (hab : gcd a b = 1) {k : } :
a * b = c ^ kc = d₁ * d₂d₁ ad₁ ^ k 0 d₁ ^ k a

theorem exists_associated_pow_of_mul_eq_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} (ha : a 0) (hb : b 0) (hab : gcd a b = 1) {k : } :
a * b = c ^ k(∃ (d : α), associated (d ^ k) a)

theorem lcm_dvd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} :
lcm a b c a c b c

theorem dvd_lcm_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
a lcm a b

theorem dvd_lcm_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
b lcm a b

theorem lcm_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} :
a bc blcm a c b

@[simp]
theorem lcm_eq_zero_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = 0 a = 0 b = 0

@[simp]
theorem normalize_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize (lcm a b) = lcm a b

theorem lcm_comm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = lcm b a

theorem lcm_assoc {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm (lcm m n) k = lcm m (lcm n k)

theorem lcm_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} :
lcm a b cc lcm a blcm a b = normalize c

theorem lcm_dvd_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c d : α} :
a bc dlcm a c lcm b d

@[simp]
theorem lcm_units_coe_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (u : units α) (a : α) :

@[simp]
theorem lcm_units_coe_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) (u : units α) :

@[simp]
theorem lcm_one_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem lcm_one_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem lcm_same {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

@[simp]
theorem lcm_eq_one_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
lcm a b = 1 a 1 b 1

@[simp]
theorem lcm_mul_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b c : α) :
lcm (a * b) (a * c) = (normalize a) * lcm b c

@[simp]
theorem lcm_mul_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b c : α) :
lcm (b * a) (c * a) = (lcm b c) * normalize a

theorem lcm_eq_left_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize a = a(lcm a b = a b a)

theorem lcm_eq_right_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a b : α) :
normalize b = b(lcm a b = b a b)

theorem lcm_dvd_lcm_mul_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm (k * m) n

theorem lcm_dvd_lcm_mul_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm (m * k) n

theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm m (k * n)

theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (m n k : α) :
lcm m n lcm m (n * k)

theorem lcm_eq_of_associated_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
lcm m k = lcm n k

theorem lcm_eq_of_associated_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
lcm k m = lcm k n

theorem units_eq_one {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique (units α)] (u : units α) :
u = 1

@[simp]
theorem norm_unit_eq_one {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique (units α)] [nontrivial α] (x : α) :

@[simp]
theorem normalize_eq {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique (units α)] [nontrivial α] (x : α) :

theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [integral_domain α] [gcd_monoid α] {a b c : α} :
a b - cgcd a b = gcd a c

theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [integral_domain α] [gcd_monoid α] {a b c : α} :
a b - cgcd b a = gcd c a

def gcd_monoid_of_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] [decidable_eq α] (gcd : α → α → α) :
(∀ (a b : α), gcd a b a)(∀ (a b : α), gcd a b b)(∀ {a b c : α}, a ca ba gcd c b)(∀ (a b : α), normalize (gcd a b) = gcd a b)gcd_monoid α

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

Equations
def gcd_monoid_of_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] [decidable_eq α] (lcm : α → α → α) :
(∀ (a b : α), a lcm a b)(∀ (a b : α), b lcm a b)(∀ {a b c : α}, c ab alcm c b a)(∀ (a b : α), normalize (lcm a b) = lcm a b)gcd_monoid α

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

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

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} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] [decidable_eq α] :
(∀ (a b : α), ∃ (c : α), ∀ (d : α), a d b d c d)gcd_monoid α

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

Equations