mathlib docs: algebra.gcd

source

@[class]

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

Type u_2

norm_unit : α → units α
norm_unit_zero : norm_unit 0 = 1
norm_unit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → norm_unit (a * b) = (norm_unit a) * norm_unit b
norm_unit_coe_units : ∀ (u : units α), norm_unit ↑u = u⁻¹

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

Instances

source

@[simp]

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

norm_unit 1 = 1

source

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

normalize = {to_fun := λ (x : α), x * ↑(norm_unit x), map_one' := _, map_mul' := _}

source

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

associated x (⇑normalize x)

source

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

associated (⇑normalize x) x

source

theorem associates.mk_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {x : α} :

associates.mk (⇑normalize x) = associates.mk x

source

@[simp]

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

⇑normalize x = x * ↑(norm_unit x)

source

@[simp]

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

⇑normalize 0 = 0

source

@[simp]

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

⇑normalize 1 = 1

source

theorem normalize_coe_units {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (u : units α) :

⇑normalize ↑u = 1

source

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

⇑normalize x = 0 ↔ x = 0

source

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

⇑normalize x = 1 ↔ is_unit x

source

@[simp]

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

norm_unit (a * ↑(norm_unit a)) = 1

source

theorem normalize_idem {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (x : α) :

⇑normalize (⇑normalize x) = ⇑normalize x

source

theorem normalize_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) :

⇑normalize a = ⇑normalize b

source

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

⇑normalize x = ⇑normalize y ↔ x ∣ y ∧ y ∣ x

source

theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] {a b : α} (ha : ⇑normalize a = a) (hb : ⇑normalize b = b) (hab : a ∣ b) (hba : b ∣ a) :

a = b

source

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

a ∣ ⇑normalize b ↔ a ∣ b

source

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

⇑normalize a ∣ b ↔ a ∣ b

source

def associates.out {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : associates α) :

α

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

Equations

associates.out = quotient.lift ⇑normalize associates.out._proof_1

source

theorem associates.out_mk {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : α) :

(associates.mk a).out = ⇑normalize a

source

@[simp]

theorem associates.out_one {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] :

1.out = 1

source

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

source

theorem associates.dvd_out_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : α) (b : associates α) :

a ∣ b.out ↔ associates.mk a ≤ b

source

theorem associates.out_dvd_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : α) (b : associates α) :

b.out ∣ a ↔ b ≤ associates.mk a

source

@[simp]

theorem associates.out_top {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] :

⊤.out = 0

source

@[simp]

theorem associates.normalize_out {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] (a : associates α) :

⇑normalize a.out = a.out

source

@[class]

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

Type u_2

norm_unit : α → units α
norm_unit_zero : gcd_monoid.norm_unit 0 = 1
norm_unit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → gcd_monoid.norm_unit (a * b) = (gcd_monoid.norm_unit a) * gcd_monoid.norm_unit b
norm_unit_coe_units : ∀ (u : units α), gcd_monoid.norm_unit ↑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_1 : α}, a ∣ c_1 → a ∣ b → a ∣ 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

int.gcd_monoid

source

@[instance]

def gcd_monoid.to_normalization_monoid (α : Type u_2) [comm_cancel_monoid_with_zero α] [nontrivial α] [s : gcd_monoid α] :

normalization_monoid α

source

@[simp]

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

⇑normalize (gcd a b) = gcd a b

source

@[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)

source

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

source

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

gcd a b = gcd b a

source

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)

source

@[instance]

def gcd_monoid.gcd.is_commutative {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :

is_commutative α gcd

source

@[instance]

def gcd_monoid.gcd.is_associative {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :

is_associative α gcd

source

theorem gcd_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) :

gcd a b = ⇑normalize c

source

@[simp]

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

gcd 0 a = ⇑normalize a

source

@[simp]

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

gcd a 0 = ⇑normalize a

source

@[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

source

@[simp]

theorem gcd_one_left {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

gcd 1 a = 1

source

@[simp]

theorem gcd_one_right {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] (a : α) :

gcd a 1 = 1

source

theorem gcd_dvd_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) :

gcd a c ∣ gcd b d

source

@[simp]

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

gcd a a = ⇑normalize a

source

@[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

source

@[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

source

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

gcd a b = a ↔ a ∣ b

source

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

gcd a b = b ↔ b ∣ a

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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

a ∣ lcm a b

source

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

b ∣ lcm a b

source

theorem lcm_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) :

lcm a c ∣ b

source

@[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

source

@[simp]

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

⇑normalize (lcm a b) = lcm a b

source

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

lcm a b = lcm b a

source

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)

source

@[instance]

def gcd_monoid.lcm.is_commutative {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :

is_commutative α lcm

source

@[instance]

def gcd_monoid.lcm.is_associative {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] :

is_associative α lcm

source

theorem lcm_eq_normalize {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) :

lcm a b = ⇑normalize c

source

theorem lcm_dvd_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) :

lcm a c ∣ lcm b d

source

@[simp]

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

lcm ↑u a = ⇑normalize a

source

@[simp]

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

lcm a ↑u = ⇑normalize a

source

@[simp]

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

lcm 1 a = ⇑normalize a

source

@[simp]

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

lcm a 1 = ⇑normalize a

source

@[simp]

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

lcm a a = ⇑normalize a

source

@[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

source

@[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

source

@[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

source

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

lcm a b = a ↔ b ∣ a

source

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

lcm a b = b ↔ a ∣ b

source

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

source

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

source

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)

source

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)

source

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

source

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

source

theorem gcd_monoid.prime_of_irreducible {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {x : α} (hi : irreducible x) :

prime x

source

theorem gcd_monoid.irreducible_iff_prime {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {p : α} :

irreducible p ↔ prime p

source

@[instance]

def int.normalization_monoid :

normalization_monoid ℤ

Equations

int.normalization_monoid = {norm_unit := λ (a : ℤ), ite (0 ≤ a) 1 (-1), norm_unit_zero := int.normalization_monoid._proof_1, norm_unit_mul := int.normalization_monoid._proof_2, norm_unit_coe_units := int.normalization_monoid._proof_3}

source

theorem int.normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) :

⇑normalize z = z

source

theorem int.normalize_of_neg {z : ℤ} (h : z < 0) :

⇑normalize z = -z

source

theorem int.normalize_coe_nat (n : ℕ) :

⇑normalize ↑n = ↑n

source

theorem int.coe_nat_abs_eq_normalize (z : ℤ) :

↑(z.nat_abs) = ⇑normalize z

source

def int.lcm (i j : ℤ) :

ℕ

ℤ specific version of least common multiple.

Equations

i.lcm j = i.nat_abs.lcm j.nat_abs

source

theorem int.lcm_def (i j : ℤ) :

i.lcm j = i.nat_abs.lcm j.nat_abs

source

theorem int.gcd_dvd_left (i j : ℤ) :

↑(i.gcd j) ∣ i

source

theorem int.gcd_dvd_right (i j : ℤ) :

↑(i.gcd j) ∣ j

source

theorem int.dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) :

k ∣ ↑(i.gcd j)

source

theorem int.gcd_mul_lcm (i j : ℤ) :

(i.gcd j) * i.lcm j = (i * j).nat_abs

source

@[instance]

def int.gcd_monoid :

gcd_monoid ℤ

Equations

int.gcd_monoid = {norm_unit := norm_unit int.normalization_monoid, norm_unit_zero := int.gcd_monoid._proof_1, norm_unit_mul := int.gcd_monoid._proof_2, norm_unit_coe_units := int.gcd_monoid._proof_3, gcd := λ (a b : ℤ), ↑(a.gcd b), lcm := λ (a b : ℤ), ↑(a.lcm b), gcd_dvd_left := int.gcd_monoid._proof_4, gcd_dvd_right := int.gcd_monoid._proof_5, dvd_gcd := int.gcd_monoid._proof_6, normalize_gcd := int.gcd_monoid._proof_7, gcd_mul_lcm := int.gcd_monoid._proof_8, lcm_zero_left := int.gcd_monoid._proof_9, lcm_zero_right := int.gcd_monoid._proof_10}