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 #

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

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 α] :

monoid_with_zero_hom α α

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

Equations

normalize = {to_fun := λ (x : α), x * ↑(norm_unit x), map_zero' := _, 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

@[protected, instance]

def comm_group_with_zero.normalization_monoid {α : Type u_1} [decidable_eq α] [comm_group_with_zero α] :

normalization_monoid α

Equations

comm_group_with_zero.normalization_monoid = {norm_unit := λ (x : α), dite (x = 0) (λ (h : x = 0), 1) (λ (h : ¬x = 0), (units.mk0 x h)⁻¹), norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}

source

@[simp]

theorem comm_group_with_zero.coe_norm_unit {α : Type u_1} [decidable_eq α] [comm_group_with_zero α] {a : α} (h0 : a ≠ 0) :

↑(norm_unit a) = a⁻¹

source

@[protected]

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

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

source

@[instance]

def gcd_monoid.to_normalization_monoid (α : Type u_2) [comm_cancel_monoid_with_zero α] [nontrivial α] [self : 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

@[protected, instance]

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

is_commutative α gcd

source

@[protected, 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 dvd_gcd_mul_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n k : α} (H : k ∣ m * n) :

k ∣ (gcd k m) * n

source

theorem dvd_mul_gcd_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {m n k : α} (H : k ∣ m * n) :

k ∣ m * gcd k n

source

theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [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.

source

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

source

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

source

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

source

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 : ℕ} (h : a * b = c ^ k) (hc : c = d₁ * d₂) (hd₁ : d₁ ∣ a) :

d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

source

theorem exists_associated_pow_of_mul_eq_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α] {a b c : α} (hab : gcd a b = 1) {k : ℕ} (h : a * b = c ^ k) :

∃ (d : α), associated (d ^ k) a

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

@[protected, instance]

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

is_commutative α lcm

source

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

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

u = 1

source

@[protected, instance]

def normalization_monoid_of_unique_units {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique (units α)] [nontrivial α] :

normalization_monoid α

Equations

normalization_monoid_of_unique_units = {norm_unit := λ (x : α), 1, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}

source

@[simp]

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

norm_unit x = 1

source

@[simp]

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

⇑normalize x = x

source

theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [integral_domain α] [gcd_monoid α] {a b c : α} (h : a ∣ b - c) :

gcd a b = gcd a c

source

theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [integral_domain α] [gcd_monoid α] {a b c : α} (h : a ∣ b - c) :

gcd b a = gcd c a

source

def normalization_monoid_of_monoid_hom_right_inverse {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [decidable_eq α] (f : associates α →* α) (hinv : function.right_inverse ⇑f associates.mk) :

normalization_monoid α

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

Equations

normalization_monoid_of_monoid_hom_right_inverse f hinv = {norm_unit := λ (a : α), ite (a = 0) 1 (classical.some _), norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}

source

def gcd_monoid_of_gcd {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] [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 ∣ c → a ∣ b → a ∣ gcd c b) (normalize_gcd : ∀ (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

gcd_monoid_of_gcd gcd gcd_dvd_left gcd_dvd_right dvd_gcd normalize_gcd = {norm_unit := norm_unit infer_instance, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _, gcd := gcd, lcm := λ (a b : α), ite (a = 0) 0 (classical.some _), gcd_dvd_left := gcd_dvd_left, gcd_dvd_right := gcd_dvd_right, dvd_gcd := _, normalize_gcd := normalize_gcd, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}

source

def gcd_monoid_of_lcm {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalization_monoid α] [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 ∣ a → b ∣ a → lcm c b ∣ a) (normalize_lcm : ∀ (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