mathlib documentation

algebra.gcd_monoid.basic

Monoids with normalization functions, gcd, and lcm #

This file defines extra structures on cancel_comm_monoid_with_zeros, including is_domains.

Main Definitions #

For the normalized_gcd_monoid instances on and , see ring_theory.int.basic.

Implementation Notes #

TODO #

Tags #

divisibility, gcd, lcm, normalize

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

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

Instances of this typeclass
Instances of other typeclasses for normalization_monoid
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
@[simp]
@[simp]
theorem normalize_eq_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {x : α} :
theorem normalize_eq_normalize {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {a b : α} (hab : a b) (hba : b a) :
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 : α} :
theorem normalize_dvd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] {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
@[simp]
@[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 α) :
theorem associates.out_dvd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalization_monoid α] (a : α) (b : associates α) :
@[simp]
@[simp]
@[class]
structure gcd_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :
Type u_2

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
@[class]
structure normalized_gcd_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :
Type u_2

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
@[simp]
theorem gcd_mul_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :
theorem dvd_gcd_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b c : α) :
theorem gcd_comm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :
theorem gcd_comm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :
theorem gcd_assoc' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
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) :
@[simp]
theorem gcd_zero_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :
@[simp]
theorem gcd_zero_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (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 : α) :
@[simp]
theorem gcd_one_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :
@[simp]
theorem gcd_one_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :
@[simp]
theorem gcd_one_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a : α) :
theorem gcd_dvd_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c d : α} (hab : a b) (hcd : c d) :
@[simp]
theorem gcd_same {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :
@[simp]
theorem gcd_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :
theorem gcd_mul_left' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b c : α) :
@[simp]
theorem gcd_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :
@[simp]
theorem gcd_mul_right' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b c : α) :
theorem gcd_eq_left_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : normalize a = a) :
theorem gcd_eq_right_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : normalize b = b) :
theorem gcd_dvd_gcd_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem gcd_dvd_gcd_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem gcd_dvd_gcd_mul_left_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem gcd_dvd_gcd_mul_right_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (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 : α) :
theorem associated.gcd_eq_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
theorem dvd_gcd_mul_of_dvd_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {m n k : α} (H : 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) :
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₁ : α) (hd₁ : d₁ m) (d₂ : α) (hd₂ : d₂ n), k = d₁ * d₂

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

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

theorem gcd_mul_dvd_mul_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (k m n : α) :
theorem gcd_pow_right_dvd_pow_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b : α} {k : } :
theorem gcd_pow_left_dvd_pow_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {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 ae be 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 ae be d) :
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) :
theorem extract_gcd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (x y : α) :
∃ (x' y' d : α), x = d * x' y = d * 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 : α} :
theorem dvd_lcm_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :
theorem dvd_lcm_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :
theorem lcm_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c : α} (hab : a b) (hcb : 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 lcm_comm {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) :
theorem lcm_comm' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (a b : α) :
theorem lcm_assoc' {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
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) :
theorem lcm_dvd_lcm {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {a b c d : α} (hab : a b) (hcd : c d) :
@[simp]
theorem lcm_units_coe_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (u : αˣ) (a : α) :
@[simp]
theorem lcm_units_coe_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) (u : αˣ) :
@[simp]
theorem lcm_one_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a : α) :
@[simp]
@[simp]
theorem lcm_same {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (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 : α) :
@[simp]
theorem lcm_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b c : α) :
theorem lcm_eq_left_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : normalize a = a) :
theorem lcm_eq_right_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] (a b : α) (h : normalize b = b) :
theorem lcm_dvd_lcm_mul_left {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem lcm_dvd_lcm_mul_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem lcm_dvd_lcm_mul_left_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (m n k : α) :
theorem lcm_dvd_lcm_mul_right_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (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 : α) :
theorem lcm_eq_of_associated_right {α : Type u_1} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α] {m n : α} (h : associated m n) (k : α) :
theorem gcd_monoid.prime_of_irreducible {α : Type u_1} [cancel_comm_monoid_with_zero α] [gcd_monoid α] {x : α} (hi : irreducible x) :
@[simp]
theorem norm_unit_eq_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (x : α) :
@[simp]
theorem normalize_eq {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] (x : α) :

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

Equations
theorem gcd_eq_of_dvd_sub_right {α : Type u_1} [comm_ring α] [is_domain α] [normalized_gcd_monoid α] {a b c : α} (h : a b - 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) :
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 ca ba gcd c b) :

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

Equations
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 ca ba 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
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 ab alcm c b a) :

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

Equations
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 ab alcm 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
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
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
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
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
@[protected, instance]
Equations
@[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) :
theorem comm_group_with_zero.normalize_eq_one (G₀ : Type u_2) [comm_group_with_zero G₀] [decidable_eq G₀] {a : G₀} (h0 : a 0) :