Documentation

class NormalizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] :

Type u_2

normUnit : α → αˣ
normUnit assigns to each element of the monoid a unit of the monoid.
normUnit_zero : normUnit 0 = 1
The proposition that normUnit maps 0 to the identity.
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
The proposition that normUnit respects multiplication of non-zero elements.
normUnit_coe_units : ∀ (u : αˣ), normUnit ↑u = u⁻¹
The proposition that normUnit maps units to their inverses.

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

Instances

@[simp]

theorem normUnit_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

normUnit 1 = 1

def normalize {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

α →*₀ α

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem associated_normalize {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (x : α) :

Associated x (↑normalize x)

theorem normalize_associated {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (x : α) :

Associated (↑normalize x) x

theorem associated_normalize_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {x : α} {y : α} :

Associated x (↑normalize y) ↔ Associated x y

theorem normalize_associated_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {x : α} {y : α} :

Associated (↑normalize x) y ↔ Associated x y

theorem Associates.mk_normalize {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (x : α) :

Associates.mk (↑normalize x) = Associates.mk x

@[simp]

theorem normalize_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (x : α) :

↑normalize x = x * ↑(normUnit x)

theorem normalize_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

↑normalize 0 = 0

theorem normalize_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

↑normalize 1 = 1

theorem normalize_coe_units {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (u : αˣ) :

↑normalize ↑u = 1

theorem normalize_eq_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {x : α} :

↑normalize x = 0 ↔ x = 0

theorem normalize_eq_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {x : α} :

↑normalize x = 1 ↔ IsUnit x

@[simp]

theorem normUnit_mul_normUnit {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : α) :

normUnit (a * ↑(normUnit a)) = 1

theorem normalize_idem {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (x : α) :

↑normalize (↑normalize x) = ↑normalize x

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

↑normalize a = ↑normalize b

theorem normalize_eq_normalize_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {x : α} {y : α} :

↑normalize x = ↑normalize y ↔ x ∣ y ∧ y ∣ x

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

a ∣ ↑normalize b ↔ a ∣ b

theorem normalize_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] {a : α} {b : α} :

↑normalize a ∣ b ↔ a ∣ b

def Associates.out {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

Associates α → α

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

Equations

Associates.out = Quotient.lift ↑normalize (_ : ∀ (a x : α), a ≈ x → ↑normalize a = ↑normalize x)

Instances For

@[simp]

theorem Associates.out_mk {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : α) :

Associates.out (Associates.mk a) = ↑normalize a

@[simp]

theorem Associates.out_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

Associates.out 1 = 1

theorem Associates.out_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : Associates α) (b : Associates α) :

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

theorem Associates.dvd_out_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : α) (b : Associates α) :

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

theorem Associates.out_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : α) (b : Associates α) :

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

@[simp]

theorem Associates.out_top {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

Associates.out ⊤ = 0

@[simp]

theorem Associates.normalize_out {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : Associates α) :

↑normalize (Associates.out a) = Associates.out a

@[simp]

theorem Associates.mk_out {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] (a : Associates α) :

Associates.mk (Associates.out a) = a

theorem Associates.out_injective {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] :

Function.Injective Associates.out

class GCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] :

Type u_2

gcd : α → α → α
The greatest common divisor between two elements.
lcm : α → α → α
The least common multiple between two elements.
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
The GCD is a divisor of the first element.
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
The GCD is a divisor of the second element.
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
Any common divisor of both elements is a divisor of the GCD.
gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)
The product of two elements is Associated with the product of their GCD and LCM.
lcm_zero_left : ∀ (a : α), lcm 0 a = 0
0 is left-absorbing.
lcm_zero_right : ∀ (a : α), lcm a 0 = 0
0 is right-absorbing.

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

class NormalizedGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends NormalizationMonoid , GCDMonoid :

Type u_2

normUnit : α → αˣ
normUnit_zero : normUnit 0 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units : ∀ (u : αˣ), normUnit ↑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 : α}, a ∣ c → a ∣ b → a ∣ gcd c b
gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)
lcm_zero_left : ∀ (a : α), lcm 0 a = 0
lcm_zero_right : ∀ (a : α), lcm a 0 = 0
normalize_gcd : ∀ (a b : α), ↑normalize (gcd a b) = gcd a b
The GCD is normalized to itself.
normalize_lcm : ∀ (a b : α), ↑normalize (lcm a b) = lcm a b
The LCM is normalized to itself.

Normalized GCD monoid: a CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) :

↑normalize (gcd a b) = gcd a b

theorem gcd_mul_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

Associated (gcd a b * lcm a b) (a * b)

theorem dvd_gcd_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) (c : α) :

a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c

theorem gcd_comm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) :

gcd a b = gcd b a

theorem gcd_comm' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

Associated (gcd a b) (gcd b a)

theorem gcd_assoc {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (m : α) (n : α) (k : α) :

gcd (gcd m n) k = gcd m (gcd n k)

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

Associated (gcd (gcd m n) k) (gcd m (gcd n k))

instance instIsCommutativeGcdToGCDMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :

IsCommutative α gcd

Equations

@instIsCommutativeGcdToGCDMonoid = @instIsCommutativeGcdToGCDMonoid.proof_1

instance instIsAssociativeGcdToGCDMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :

IsAssociative α gcd

Equations

@instIsAssociativeGcdToGCDMonoid = @instIsAssociativeGcdToGCDMonoid.proof_1

theorem gcd_eq_normalize {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) :

gcd a b = ↑normalize c

@[simp]

theorem gcd_zero_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

gcd 0 a = ↑normalize a

theorem gcd_zero_left' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) :

Associated (gcd 0 a) a

@[simp]

theorem gcd_zero_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

gcd a 0 = ↑normalize a

theorem gcd_zero_right' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) :

Associated (gcd a 0) a

@[simp]

theorem gcd_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

gcd a b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem gcd_one_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

gcd 1 a = 1

@[simp]

theorem gcd_one_left' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) :

Associated (gcd 1 a) 1

@[simp]

theorem gcd_one_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

gcd a 1 = 1

@[simp]

theorem gcd_one_right' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) :

Associated (gcd a 1) 1

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

gcd a c ∣ gcd b d

@[simp]

theorem gcd_same {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

gcd a a = ↑normalize a

@[simp]

theorem gcd_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :

gcd (a * b) (a * c) = ↑normalize a * gcd b c

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

Associated (gcd (a * b) (a * c)) (a * gcd b c)

@[simp]

theorem gcd_mul_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :

gcd (b * a) (c * a) = gcd b c * ↑normalize a

@[simp]

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

Associated (gcd (b * a) (c * a)) (gcd b c * a)

theorem gcd_eq_left_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (h : ↑normalize a = a) :

gcd a b = a ↔ a ∣ b

theorem gcd_eq_right_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (h : ↑normalize b = b) :

gcd a b = b ↔ b ∣ a

theorem gcd_dvd_gcd_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

gcd m n ∣ gcd (k * m) n

theorem gcd_dvd_gcd_mul_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

gcd m n ∣ gcd (m * k) n

theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

gcd m n ∣ gcd m (k * n)

theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

gcd m n ∣ gcd m (n * k)

theorem Associated.gcd_eq_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :

gcd m k = gcd n k

theorem Associated.gcd_eq_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :

gcd k m = gcd k n

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

k ∣ gcd k m * n

theorem dvd_gcd_mul_iff_dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {m : α} {n : α} {k : α} :

k ∣ gcd k m * n ↔ k ∣ m * n

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

k ∣ m * gcd k n

theorem dvd_mul_gcd_iff_dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {m : α} {n : α} {k : α} :

k ∣ m * gcd k n ↔ k ∣ m * n

theorem exists_dvd_and_dvd_of_dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {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 GCDMonoid 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.prodDvdAndDvdOfDvdProd for a constructive version on ℕ.

theorem dvd_mul {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {k : α} {m : α} {n : α} :

k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂

theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (k : α) (m : α) (n : α) :

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

theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {a : α} {b : α} {k : ℕ} :

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

theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {a : α} {b : α} {k : ℕ} :

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

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

∃ d, a = d ^ k

theorem gcd_greatest {α : Type u_2} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} {b : α} {d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) :

gcd a b = ↑normalize d

theorem gcd_greatest_associated {α : Type u_2} [CancelCommMonoidWithZero α] [GCDMonoid α] {a : α} {b : α} {d : α} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d) :

Associated d (gcd a b)

theorem isUnit_gcd_of_eq_mul_gcd {α : Type u_2} [CancelCommMonoidWithZero α] [GCDMonoid α] {x : α} {y : α} {x' : α} {y' : α} (ex : x = gcd x y * x') (ey : y = gcd x y * y') (h : gcd x y ≠ 0) :

IsUnit (gcd x' y')

theorem extract_gcd {α : Type u_2} [CancelCommMonoidWithZero α] [GCDMonoid α] (x : α) (y : α) :

∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')

theorem associated_gcd_left_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {x : α} {y : α} :

Associated x (gcd x y) ↔ x ∣ y

theorem associated_gcd_right_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {x : α} {y : α} :

Associated y (gcd x y) ↔ y ∣ x

theorem Irreducible.isUnit_gcd_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {x : α} {y : α} (hx : Irreducible x) :

IsUnit (gcd x y) ↔ ¬x ∣ y

theorem Irreducible.gcd_eq_one_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {x : α} {y : α} (hx : Irreducible x) :

gcd x y = 1 ↔ ¬x ∣ y

theorem lcm_dvd_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {a : α} {b : α} {c : α} :

lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

theorem dvd_lcm_left {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

a ∣ lcm a b

theorem dvd_lcm_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

b ∣ lcm a b

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

lcm a c ∣ b

@[simp]

theorem lcm_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

lcm a b = 0 ↔ a = 0 ∨ b = 0

@[simp]

theorem normalize_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) :

↑normalize (lcm a b) = lcm a b

theorem lcm_comm {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) :

lcm a b = lcm b a

theorem lcm_comm' {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) (b : α) :

Associated (lcm a b) (lcm b a)

theorem lcm_assoc {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (m : α) (n : α) (k : α) :

lcm (lcm m n) k = lcm m (lcm n k)

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

Associated (lcm (lcm m n) k) (lcm m (lcm n k))

instance instIsCommutativeLcmToGCDMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :

IsCommutative α lcm

Equations

@instIsCommutativeLcmToGCDMonoid = @instIsCommutativeLcmToGCDMonoid.proof_1

instance instIsAssociativeLcmToGCDMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] :

IsAssociative α lcm

Equations

@instIsAssociativeLcmToGCDMonoid = @instIsAssociativeLcmToGCDMonoid.proof_1

theorem lcm_eq_normalize {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) :

lcm a b = ↑normalize c

theorem lcm_dvd_lcm {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {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} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (u : αˣ) (a : α) :

lcm (↑u) a = ↑normalize a

@[simp]

theorem lcm_units_coe_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (u : αˣ) :

lcm a ↑u = ↑normalize a

@[simp]

theorem lcm_one_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

lcm 1 a = ↑normalize a

@[simp]

theorem lcm_one_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

lcm a 1 = ↑normalize a

@[simp]

theorem lcm_same {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) :

lcm a a = ↑normalize a

@[simp]

theorem lcm_eq_one_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) :

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

@[simp]

theorem lcm_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :

lcm (a * b) (a * c) = ↑normalize a * lcm b c

@[simp]

theorem lcm_mul_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (c : α) :

lcm (b * a) (c * a) = lcm b c * ↑normalize a

theorem lcm_eq_left_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (h : ↑normalize a = a) :

lcm a b = a ↔ b ∣ a

theorem lcm_eq_right_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] (a : α) (b : α) (h : ↑normalize b = b) :

lcm a b = b ↔ a ∣ b

theorem lcm_dvd_lcm_mul_left {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

lcm m n ∣ lcm (k * m) n

theorem lcm_dvd_lcm_mul_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

lcm m n ∣ lcm (m * k) n

theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

lcm m n ∣ lcm m (k * n)

theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] (m : α) (n : α) (k : α) :

lcm m n ∣ lcm m (n * k)

theorem lcm_eq_of_associated_left {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :

lcm m k = lcm n k

theorem lcm_eq_of_associated_right {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {m : α} {n : α} (h : Associated m n) (k : α) :

lcm k m = lcm k n

theorem GCDMonoid.prime_of_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {x : α} (hi : Irreducible x) :

Prime x

theorem GCDMonoid.irreducible_iff_prime {α : Type u_1} [CancelCommMonoidWithZero α] [GCDMonoid α] {p : α} :

Irreducible p ↔ Prime p

instance normalizationMonoidOfUniqueUnits {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

NormalizationMonoid α

Equations

One or more equations did not get rendered due to their size.

instance uniqueNormalizationMonoidOfUniqueUnits {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

Unique (NormalizationMonoid α)

Equations

uniqueNormalizationMonoidOfUniqueUnits = { toInhabited := { default := normalizationMonoidOfUniqueUnits }, uniq := (_ : ∀ (x : NormalizationMonoid α), x = default) }

instance subsingleton_gcdMonoid_of_unique_units {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

Subsingleton (GCDMonoid α)

Equations

@subsingleton_gcdMonoid_of_unique_units = @subsingleton_gcdMonoid_of_unique_units.proof_1

instance subsingleton_normalizedGCDMonoid_of_unique_units {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

Subsingleton (NormalizedGCDMonoid α)

Equations

@subsingleton_normalizedGCDMonoid_of_unique_units = @subsingleton_normalizedGCDMonoid_of_unique_units.proof_1

@[simp]

theorem normUnit_eq_one {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] (x : α) :

normUnit x = 1

theorem normalize_eq {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] (x : α) :

↑normalize x = x

@[simp]

theorem associatesEquivOfUniqueUnits_apply {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

∀ (a : Associates α), ↑associatesEquivOfUniqueUnits a = Associates.out a

@[simp]

theorem associatesEquivOfUniqueUnits_symm_apply {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] (a : α) :

↑(MulEquiv.symm associatesEquivOfUniqueUnits) a = Associates.mk a

def associatesEquivOfUniqueUnits {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] :

Associates α ≃* α

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [CommRing α] [IsDomain α] [NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (h : a ∣ b - c) :

gcd a b = gcd a c

theorem gcd_eq_of_dvd_sub_left {α : Type u_1} [CommRing α] [IsDomain α] [NormalizedGCDMonoid α] {a : α} {b : α} {c : α} (h : a ∣ b - c) :

gcd b a = gcd c a

def normalizationMonoidOfMonoidHomRightInverse {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] (f : Associates α →* α) (hinv : Function.RightInverse (↑f) Associates.mk) :

NormalizationMonoid α

Define NormalizationMonoid on a structure from a MonoidHom inverse to Associates.mk.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def gcdMonoidOfGCD {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] (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 GCDMonoid on a structure just from the gcd and its properties.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def normalizedGCDMonoidOfGCD {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [DecidableEq α] (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 NormalizedGCDMonoid on a structure just from the gcd and its properties.

Equations

normalizedGCDMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right dvd_gcd normalize_gcd = let src := inferInstance; NormalizedGCDMonoid.mk normalize_gcd (_ : ∀ (a b : α), ↑normalize (lcm a b) = lcm a b)

Instances For

noncomputable def gcdMonoidOfLCM {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] (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 GCDMonoid on a structure just from the lcm and its properties.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def normalizedGCDMonoidOfLCM {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [DecidableEq α] (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 NormalizedGCDMonoid on a structure just from the lcm and its properties.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def gcdMonoidOfExistsGCD {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] (h : ∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def normalizedGCDMonoidOfExistsGCD {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def gcdMonoidOfExistsLCM {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] (h : ∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def normalizedGCDMonoidOfExistsLCM {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [DecidableEq α] (h : ∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CommGroupWithZero.instNormalizedGCDMonoidToCancelCommMonoidWithZero (G₀ : Type u_2) [CommGroupWithZero G₀] [DecidableEq G₀] :

NormalizedGCDMonoid G₀

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroupWithZero.coe_normUnit (G₀ : Type u_2) [CommGroupWithZero G₀] [DecidableEq G₀] {a : G₀} (h0 : a ≠ 0) :

↑(normUnit a) = a⁻¹