mathlib3 documentation

@[class]

structure normalization_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :

Type u_2

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

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

Instances of this typeclass

Instances of other typeclasses for normalization_monoid

normalization_monoid.has_sizeof_inst
unique_normalization_monoid_of_unique_units
unique_factorization_monoid.normalization_monoid.inhabited

@[simp]

theorem norm_unit_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] :

normalization_monoid.norm_unit 1 = 1

def normalize {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] :

α →*₀ α

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

Equations

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

theorem associated_normalize {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (x : α) :

associated x (⇑normalize x)

theorem normalize_associated {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (x : α) :

associated (⇑normalize x) x

theorem associated_normalize_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {x y : α} :

associated x (⇑normalize y) ↔ associated x y

theorem normalize_associated_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {x y : α} :

associated (⇑normalize x) y ↔ associated x y

theorem associates.mk_normalize {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (x : α) :

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

@[simp]

theorem normalize_apply {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (x : α) :

⇑normalize x = x * ↑(normalization_monoid.norm_unit x)

@[simp]

theorem normalize_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] :

⇑normalize 0 = 0

@[simp]

theorem normalize_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] :

⇑normalize 1 = 1

theorem normalize_coe_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (u : αˣ) :

⇑normalize ↑u = 1

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

⇑normalize x = 0 ↔ x = 0

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

⇑normalize x = 1 ↔ is_unit x

@[simp]

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

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

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

⇑normalize (⇑normalize x) = ⇑normalize x

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

⇑normalize a = ⇑normalize b

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

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

theorem dvd_antisymm_of_normalize_eq {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {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} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {a b : α} :

a ∣ ⇑normalize b ↔ a ∣ b

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

⇑normalize a ∣ b ↔ a ∣ b

@[protected]

def associates.out {α : Type u_1} [cancel_comm_monoid_with_zero α] [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

@[simp]

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

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

@[simp]

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

1.out = 1

theorem associates.out_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (a b : associates α) :

(a * b).out = a.out * b.out

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

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

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

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

@[simp]

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

⊤.out = 0

@[simp]

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

⇑normalize a.out = a.out

@[simp]

theorem associates.mk_out {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (a : associates α) :

associates.mk a.out = a

function.injective associates.out

theorem associates.out_injective {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] :

@[class]

structure gcd_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :

Type u_2

gcd : α → α → α
lcm : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd_monoid.gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd_monoid.gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd_monoid.gcd c b
gcd_mul_lcm : ∀ (a b : α), associated (gcd_monoid.gcd a b * gcd_monoid.lcm a b) (a * b)
lcm_zero_left : ∀ (a : α), gcd_monoid.lcm 0 a = 0
lcm_zero_right : ∀ (a : α), gcd_monoid.lcm a 0 = 0

GCD monoid: a cancel_comm_monoid_with_zero 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.

Instances of this typeclass

Instances of other typeclasses for gcd_monoid

gcd_monoid.has_sizeof_inst
subsingleton_gcd_monoid_of_unique_units

@[class]

structure normalized_gcd_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :

Type u_2

to_normalization_monoid : normalization_monoid α
to_gcd_monoid : gcd_monoid α
normalize_gcd : ∀ (a b : α), ⇑normalize (gcd_monoid.gcd a b) = gcd_monoid.gcd a b
normalize_lcm : ∀ (a b : α), ⇑normalize (gcd_monoid.lcm a b) = gcd_monoid.lcm a b

Normalized GCD monoid: a cancel_comm_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 of this typeclass

Instances of other typeclasses for normalized_gcd_monoid

normalized_gcd_monoid.has_sizeof_inst
subsingleton_normalized_gcd_monoid_of_unique_units

@[simp]

theorem normalize_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :

⇑normalize (gcd_monoid.gcd a b) = gcd_monoid.gcd a b

theorem gcd_mul_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :

associated (gcd_monoid.gcd a b * gcd_monoid.lcm a b) (a * b)

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

a ∣ gcd_monoid.gcd b c ↔ a ∣ b ∧ a ∣ c

theorem gcd_comm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :

gcd_monoid.gcd a b = gcd_monoid.gcd b a

theorem gcd_comm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :

associated (gcd_monoid.gcd a b) (gcd_monoid.gcd b a)

theorem gcd_assoc {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (m n k : α) :

gcd_monoid.gcd (gcd_monoid.gcd m n) k = gcd_monoid.gcd m (gcd_monoid.gcd n k)

theorem gcd_assoc' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

associated (gcd_monoid.gcd (gcd_monoid.gcd m n) k) (gcd_monoid.gcd m (gcd_monoid.gcd n k))

@[protected, instance]

def gcd_monoid.gcd.is_commutative {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

is_commutative α gcd_monoid.gcd

@[protected, instance]

def gcd_monoid.gcd.is_associative {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

is_associative α gcd_monoid.gcd

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

gcd_monoid.gcd a b = ⇑normalize c

@[simp]

theorem gcd_zero_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.gcd 0 a = ⇑normalize a

theorem gcd_zero_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :

associated (gcd_monoid.gcd 0 a) a

@[simp]

theorem gcd_zero_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.gcd a 0 = ⇑normalize a

theorem gcd_zero_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :

associated (gcd_monoid.gcd a 0) a

@[simp]

theorem gcd_eq_zero_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :

gcd_monoid.gcd a b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem gcd_one_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.gcd 1 a = 1

@[simp]

theorem gcd_one_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :

associated (gcd_monoid.gcd 1 a) 1

@[simp]

theorem gcd_one_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.gcd a 1 = 1

@[simp]

theorem gcd_one_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :

associated (gcd_monoid.gcd a 1) 1

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

gcd_monoid.gcd a c ∣ gcd_monoid.gcd b d

@[simp]

theorem gcd_same {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.gcd a a = ⇑normalize a

@[simp]

theorem gcd_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :

gcd_monoid.gcd (a * b) (a * c) = ⇑normalize a * gcd_monoid.gcd b c

theorem gcd_mul_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b c : α) :

associated (gcd_monoid.gcd (a * b) (a * c)) (a * gcd_monoid.gcd b c)

@[simp]

theorem gcd_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :

gcd_monoid.gcd (b * a) (c * a) = gcd_monoid.gcd b c * ⇑normalize a

@[simp]

theorem gcd_mul_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b c : α) :

associated (gcd_monoid.gcd (b * a) (c * a)) (gcd_monoid.gcd b c * a)

theorem gcd_eq_left_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : ⇑normalize a = a) :

gcd_monoid.gcd a b = a ↔ a ∣ b

theorem gcd_eq_right_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : ⇑normalize b = b) :

gcd_monoid.gcd a b = b ↔ b ∣ a

theorem gcd_dvd_gcd_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.gcd m n ∣ gcd_monoid.gcd (k * m) n

theorem gcd_dvd_gcd_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.gcd m n ∣ gcd_monoid.gcd (m * k) n

theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.gcd m n ∣ gcd_monoid.gcd m (k * n)

theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.gcd m n ∣ gcd_monoid.gcd m (n * k)

theorem associated.gcd_eq_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :

gcd_monoid.gcd m k = gcd_monoid.gcd n k

theorem associated.gcd_eq_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :

gcd_monoid.gcd k m = gcd_monoid.gcd k n

theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {m n k : α} (H : k ∣ m * n) :

k ∣ gcd_monoid.gcd k m * n

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

k ∣ m * gcd_monoid.gcd k n

theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {m n k : α} (H : k ∣ m * n) :

∃ (d₁ d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

In other words, the nonzero elements of a gcd_monoid form a decomposition monoid (more widely known as a pre-Schreier domain in the context of rings).

Note: In general, this representation is highly non-unique.

See nat.prod_dvd_and_dvd_of_dvd_prod for a constructive version on ℕ.

theorem dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {k m n : α} :

k ∣ m * n ↔ ∃ (d₁ d₂ : α), d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (k m n : α) :

gcd_monoid.gcd k (m * n) ∣ gcd_monoid.gcd k m * gcd_monoid.gcd k n

theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b : α} {k : ℕ} :

gcd_monoid.gcd a (b ^ k) ∣ gcd_monoid.gcd a b ^ k

theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b : α} {k : ℕ} :

gcd_monoid.gcd (a ^ k) b ∣ gcd_monoid.gcd a b ^ k

theorem pow_dvd_of_mul_eq_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c d₁ d₂ : α} (ha : a ≠ 0) (hab : is_unit (gcd_monoid.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} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c : α} (hab : is_unit (gcd_monoid.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} [cancel_comm_monoid_with_zero α] [gcd_monoid α] [unique αˣ] {a b c : α} (hab : is_unit (gcd_monoid.gcd a b)) {k : ℕ} (h : a * b = c ^ k) :

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

theorem gcd_greatest {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) :

gcd_monoid.gcd a b = ⇑normalize d

theorem gcd_greatest_associated {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) :

associated d (gcd_monoid.gcd a b)

theorem is_unit_gcd_of_eq_mul_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {x y x' y' : α} (ex : x = gcd_monoid.gcd x y * x') (ey : y = gcd_monoid.gcd x y * y') (h : gcd_monoid.gcd x y ≠ 0) :

is_unit (gcd_monoid.gcd x' y')

theorem extract_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (x y : α) :

∃ (x' y' : α), x = gcd_monoid.gcd x y * x' ∧ y = gcd_monoid.gcd x y * y' ∧ is_unit (gcd_monoid.gcd x' y')

theorem lcm_dvd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c : α} :

gcd_monoid.lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

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

a ∣ gcd_monoid.lcm a b

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

b ∣ gcd_monoid.lcm a b

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

gcd_monoid.lcm a c ∣ b

@[simp]

theorem lcm_eq_zero_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :

gcd_monoid.lcm a b = 0 ↔ a = 0 ∨ b = 0

@[simp]

theorem normalize_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :

⇑normalize (gcd_monoid.lcm a b) = gcd_monoid.lcm a b

theorem lcm_comm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :

gcd_monoid.lcm a b = gcd_monoid.lcm b a

theorem lcm_comm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :

associated (gcd_monoid.lcm a b) (gcd_monoid.lcm b a)

theorem lcm_assoc {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (m n k : α) :

gcd_monoid.lcm (gcd_monoid.lcm m n) k = gcd_monoid.lcm m (gcd_monoid.lcm n k)

theorem lcm_assoc' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

associated (gcd_monoid.lcm (gcd_monoid.lcm m n) k) (gcd_monoid.lcm m (gcd_monoid.lcm n k))

@[protected, instance]

def gcd_monoid.lcm.is_commutative {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

is_commutative α gcd_monoid.lcm

@[protected, instance]

def gcd_monoid.lcm.is_associative {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] :

is_associative α gcd_monoid.lcm

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

gcd_monoid.lcm a b = ⇑normalize c

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

gcd_monoid.lcm a c ∣ gcd_monoid.lcm b d

@[simp]

theorem lcm_units_coe_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (u : αˣ) (a : α) :

gcd_monoid.lcm ↑u a = ⇑normalize a

@[simp]

theorem lcm_units_coe_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (u : αˣ) :

gcd_monoid.lcm a ↑u = ⇑normalize a

@[simp]

theorem lcm_one_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.lcm 1 a = ⇑normalize a

@[simp]

theorem lcm_one_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.lcm a 1 = ⇑normalize a

@[simp]

theorem lcm_same {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :

gcd_monoid.lcm a a = ⇑normalize a

@[simp]

theorem lcm_eq_one_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :

gcd_monoid.lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1

@[simp]

theorem lcm_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :

gcd_monoid.lcm (a * b) (a * c) = ⇑normalize a * gcd_monoid.lcm b c

@[simp]

theorem lcm_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :

gcd_monoid.lcm (b * a) (c * a) = gcd_monoid.lcm b c * ⇑normalize a

theorem lcm_eq_left_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : ⇑normalize a = a) :

gcd_monoid.lcm a b = a ↔ b ∣ a

theorem lcm_eq_right_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : ⇑normalize b = b) :

gcd_monoid.lcm a b = b ↔ a ∣ b

theorem lcm_dvd_lcm_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.lcm m n ∣ gcd_monoid.lcm (k * m) n

theorem lcm_dvd_lcm_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.lcm m n ∣ gcd_monoid.lcm (m * k) n

theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.lcm m n ∣ gcd_monoid.lcm m (k * n)

theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :

gcd_monoid.lcm m n ∣ gcd_monoid.lcm m (n * k)

theorem lcm_eq_of_associated_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :

gcd_monoid.lcm m k = gcd_monoid.lcm n k

theorem lcm_eq_of_associated_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :

gcd_monoid.lcm k m = gcd_monoid.lcm k n

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

prime x

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

irreducible p ↔ prime p

@[protected, instance]

def normalization_monoid_of_unique_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] :

normalization_monoid α

Equations

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

@[protected, instance]

def unique_normalization_monoid_of_unique_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] :

unique (normalization_monoid α)

Equations

unique_normalization_monoid_of_unique_units = {to_inhabited := {default := normalization_monoid_of_unique_units _inst_2}, uniq := _}

@[protected, instance]

def subsingleton_gcd_monoid_of_unique_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] :

subsingleton (gcd_monoid α)

@[protected, instance]

def subsingleton_normalized_gcd_monoid_of_unique_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] :

subsingleton (normalized_gcd_monoid α)

@[simp]

theorem norm_unit_eq_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (x : α) :

normalization_monoid.norm_unit x = 1

@[simp]

theorem normalize_eq {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (x : α) :

⇑normalize x = x

@[simp]

theorem associates_equiv_of_unique_units_apply {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (ᾰ : associates α) :

⇑associates_equiv_of_unique_units ᾰ = ᾰ.out

def associates_equiv_of_unique_units {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] :

associates α ≃* α

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

Equations

associates_equiv_of_unique_units = {to_fun := associates.out normalization_monoid_of_unique_units, inv_fun := associates.mk (monoid_with_zero.to_monoid α), left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem associates_equiv_of_unique_units_symm_apply {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (a : α) :

⇑(associates_equiv_of_unique_units.symm) a = associates.mk a

theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [comm_ring α] [is_domain α] [normalized_gcd_monoid α] {a b c : α} (h : a ∣ b - c) :

gcd_monoid.gcd a b = gcd_monoid.gcd a c

theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [comm_ring α] [is_domain α] [normalized_gcd_monoid α] {a b c : α} (h : a ∣ b - c) :

gcd_monoid.gcd b a = gcd_monoid.gcd c a

noncomputable def normalization_monoid_of_monoid_hom_right_inverse {α : Type u_1} [cancel_comm_monoid_with_zero α] [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 := _}

noncomputable def gcd_monoid_of_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [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) :

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 = {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 := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}

noncomputable def normalized_gcd_monoid_of_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [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) :

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

Equations

normalized_gcd_monoid_of_gcd gcd gcd_dvd_left gcd_dvd_right dvd_gcd normalize_gcd = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit infer_instance, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}, to_gcd_monoid := {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 := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}, normalize_gcd := normalize_gcd, normalize_lcm := _}

noncomputable def gcd_monoid_of_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [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) :

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

Equations

gcd_monoid_of_lcm lcm dvd_lcm_left dvd_lcm_right lcm_dvd = let exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := _ in {gcd := λ (a b : α), ite (a = 0) b (ite (b = 0) a (classical.some _)), lcm := lcm, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}

noncomputable def normalized_gcd_monoid_of_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [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) :

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

Equations

normalized_gcd_monoid_of_lcm lcm dvd_lcm_left dvd_lcm_right lcm_dvd normalize_lcm = let exists_gcd : ∀ (a b : α), lcm a b ∣ ⇑normalize (a * b) := _ in {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit infer_instance, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}, to_gcd_monoid := {gcd := λ (a b : α), ite (a = 0) (⇑normalize b) (ite (b = 0) (⇑normalize a) (classical.some _)), lcm := lcm, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}, normalize_gcd := _, normalize_lcm := normalize_lcm}

noncomputable def gcd_monoid_of_exists_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [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

gcd_monoid_of_exists_gcd h = gcd_monoid_of_gcd (λ (a b : α), classical.some _) _ _ _

noncomputable def normalized_gcd_monoid_of_exists_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] [decidable_eq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) :

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

Equations

normalized_gcd_monoid_of_exists_gcd h = normalized_gcd_monoid_of_gcd (λ (a b : α), ⇑normalize (classical.some _)) _ _ _ _

noncomputable def gcd_monoid_of_exists_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [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

gcd_monoid_of_exists_lcm h = gcd_monoid_of_lcm (λ (a b : α), classical.some _) _ _ _

noncomputable def normalized_gcd_monoid_of_exists_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] [decidable_eq α] (h : ∀ (a b : α), ∃ (c : α), ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) :

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

Equations

normalized_gcd_monoid_of_exists_lcm h = normalized_gcd_monoid_of_lcm (λ (a b : α), ⇑normalize (classical.some _)) _ _ _ _

@[protected, instance]

def comm_group_with_zero.normalized_gcd_monoid (G₀ : Type u_2) [comm_group_with_zero G₀] [decidable_eq G₀] :

normalized_gcd_monoid G₀

Equations

comm_group_with_zero.normalized_gcd_monoid G₀ = {to_normalization_monoid := {norm_unit := λ (x : G₀), dite (x = 0) (λ (h : x = 0), 1) (λ (h : ¬x = 0), (units.mk0 x h)⁻¹), norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}, to_gcd_monoid := {gcd := λ (a b : G₀), ite (a = 0 ∧ b = 0) 0 1, lcm := λ (a b : G₀), ite (a = 0 ∨ b = 0) 0 1, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}, normalize_gcd := _, normalize_lcm := _}

@[simp]

theorem comm_group_with_zero.coe_norm_unit (G₀ : Type u_2) [comm_group_with_zero G₀] [decidable_eq G₀] {a : G₀} (h0 : a ≠ 0) :

↑(normalization_monoid.norm_unit a) = a⁻¹