Mathlib.Algebra.GCDMonoid.Nat

instGCDMonoidNat instance

: GCDMonoid ℕ

Full source

/-- `ℕ` is a gcd_monoid. -/
instance : GCDMonoid ℕ where
  gcd := Nat.gcd
  lcm := Nat.lcm
  gcd_dvd_left := Nat.gcd_dvd_left
  gcd_dvd_right := Nat.gcd_dvd_right
  dvd_gcd := Nat.dvd_gcd
  gcd_mul_lcm a b := by rw [Nat.gcd_mul_lcm]; rfl
  lcm_zero_left := Nat.lcm_zero_left
  lcm_zero_right := Nat.lcm_zero_right

Natural Numbers as a GCD Monoid

Informal description

The natural numbers $\mathbb{N}$ form a GCD monoid, where the greatest common divisor and least common multiple operations are given by the standard definitions on $\mathbb{N}$.

gcd_eq_nat_gcd theorem

(m n : ℕ) : gcd m n = Nat.gcd m n

Full source

theorem gcd_eq_nat_gcd (m n : ℕ) : gcd m n = Nat.gcd m n :=
  rfl

Equivalence of GCD Monoid GCD and Natural Number GCD

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ in the GCD monoid structure on $\mathbb{N}$ is equal to the standard natural number GCD $\text{Nat.gcd}(m, n)$.

lcm_eq_nat_lcm theorem

(m n : ℕ) : lcm m n = Nat.lcm m n

Full source

theorem lcm_eq_nat_lcm (m n : ℕ) : lcm m n = Nat.lcm m n :=
  rfl

Equivalence of GCD Monoid LCM and Natural Number LCM

Informal description

For any natural numbers $m$ and $n$, the least common multiple $\text{lcm}(m, n)$ in the GCD monoid structure on $\mathbb{N}$ is equal to the standard natural number LCM $\text{Nat.lcm}(m, n)$.

instNormalizedGCDMonoidNat instance

: NormalizedGCDMonoid ℕ

Full source

instance : NormalizedGCDMonoid ℕ :=
  { (inferInstance : GCDMonoid ℕ),
    (inferInstance : NormalizationMonoid ℕ) with
    normalize_gcd := fun _ _ => normalize_eq _
    normalize_lcm := fun _ _ => normalize_eq _ }

Natural Numbers as a Normalized GCD Monoid

Informal description

The natural numbers $\mathbb{N}$ form a normalized GCD monoid, where the greatest common divisor and least common multiple operations are given by the standard definitions on $\mathbb{N}$, and the normalization function is the identity map.

Int.normalizationMonoid instance

: NormalizationMonoid ℤ

Full source

instance normalizationMonoid : NormalizationMonoid ℤ where
  normUnit a := if 0 ≤ a then 1 else -1
  normUnit_zero := if_pos le_rfl
  normUnit_mul {a b} hna hnb := by
    rcases hna.lt_or_lt with ha | ha <;> rcases hnb.lt_or_lt with hb | hb <;>
      simp [Int.mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
  normUnit_coe_units u :=
    (units_eq_one_or u).elim (fun eq => eq.symm ▸ if_pos Int.one_nonneg) fun eq =>
      eq.symm ▸ if_neg (not_le_of_gt <| show (-1 : ℤ) < 0 by decide)

Normalization Monoid Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a normalization monoid, where the normalization function maps each integer to its non-negative counterpart (i.e., $\text{normalize}(z) = |z|$) and the unit normalization function is defined by $\text{normUnit}(z) = 1$ if $z \geq 0$ and $\text{normUnit}(z) = -1$ otherwise.

Int.normUnit_eq theorem

(z : ℤ) : normUnit z = if 0 ≤ z then 1 else -1

Full source

theorem normUnit_eq (z : ℤ) : normUnit z = if 0 ≤ z then 1 else -1 := rfl

Normalization Unit Condition for Integers: $\text{normUnit}(z) = \begin{cases} 1 & \text{if } z \geq 0 \\ -1 & \text{otherwise} \end{cases}$

Informal description

For any integer $z$, the normalization unit $\text{normUnit}(z)$ is equal to $1$ if $z \geq 0$ and $-1$ otherwise.

Int.normalize_of_nonneg theorem

{z : ℤ} (h : 0 ≤ z) : normalize z = z

Full source

theorem normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z := by
  rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]

Normalization of Non-Negative Integers is Identity

Informal description

For any integer $z$ such that $z \geq 0$, the normalization of $z$ is equal to $z$ itself, i.e., $\text{normalize}(z) = z$.

Int.normalize_of_nonpos theorem

{z : ℤ} (h : z ≤ 0) : normalize z = -z

Full source

theorem normalize_of_nonpos {z : ℤ} (h : z ≤ 0) : normalize z = -z := by
  obtain rfl | h := h.eq_or_lt
  · simp
  · rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
      mul_neg_one]

Normalization of Non-Positive Integers Equals Negation

Informal description

For any integer $z$ such that $z \leq 0$, the normalization of $z$ is equal to $-z$, i.e., $\text{normalize}(z) = -z$.

Int.normalize_coe_nat theorem

(n : ℕ) : normalize (n : ℤ) = n

Full source

theorem normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
  normalize_of_nonneg (ofNat_le_ofNat_of_le <| Nat.zero_le n)

Normalization Preserves Natural Numbers in Integers

Informal description

For any natural number $n$, the normalization of the integer $n$ (viewed as an element of $\mathbb{Z}$) is equal to $n$ itself, i.e., $\text{normalize}(n) = n$.

Int.abs_eq_normalize theorem

(z : ℤ) : |z| = normalize z

Full source

theorem abs_eq_normalize (z : ℤ) : |z| = normalize z := by
  cases le_total 0 z <;>
  simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

Absolute Value Equals Normalization in Integers

Informal description

For any integer $z$, the absolute value of $z$ equals its normalization, i.e., $|z| = \text{normalize}(z)$.

Int.nonneg_of_normalize_eq_self theorem

{z : ℤ} (hz : normalize z = z) : 0 ≤ z

Full source

theorem nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) : 0 ≤ z := by
  by_cases h : 0 ≤ z
  · exact h
  · rw [normalize_of_nonpos (le_of_not_le h)] at hz
    omega

Non-Negativity from Self-Normalization in Integers

Informal description

For any integer $z$, if the normalization of $z$ equals $z$ itself (i.e., $\text{normalize}(z) = z$), then $z$ is non-negative (i.e., $0 \leq z$).

Int.nonneg_iff_normalize_eq_self theorem

(z : ℤ) : normalize z = z ↔ 0 ≤ z

Full source

theorem nonneg_iff_normalize_eq_self (z : ℤ) : normalizenormalize z = z ↔ 0 ≤ z :=
  ⟨nonneg_of_normalize_eq_self, normalize_of_nonneg⟩

Characterization of Non-Negative Integers via Normalization: $\text{normalize}(z) = z \leftrightarrow z \geq 0$

Informal description

For any integer $z$, the normalization of $z$ equals $z$ itself if and only if $z$ is non-negative, i.e., $\text{normalize}(z) = z \leftrightarrow 0 \leq z$.

Int.instGCDMonoid instance

: GCDMonoid ℤ

Full source

instance : GCDMonoid ℤ where
  gcd a b := Int.gcd a b
  lcm a b := Int.lcm a b
  gcd_dvd_left _ _ := Int.gcd_dvd_left
  gcd_dvd_right _ _ := Int.gcd_dvd_right
  dvd_gcd := dvd_coe_gcd
  gcd_mul_lcm a b := by
    rw [← Int.natCast_mul, gcd_mul_lcm, natCast_natAbs, abs_eq_normalize]
    exact normalize_associated (a * b)
  lcm_zero_left _ := natCast_eq_zero.2 <| Nat.lcm_zero_left _
  lcm_zero_right _ := natCast_eq_zero.2 <| Nat.lcm_zero_right _

Integers as a GCD Monoid

Informal description

The integers $\mathbb{Z}$ form a GCD monoid, meaning they have a well-defined greatest common divisor operation that satisfies the properties of a GCD monoid.

Int.instNormalizedGCDMonoid instance

: NormalizedGCDMonoid ℤ

Full source

instance : NormalizedGCDMonoid ℤ :=
  { Int.normalizationMonoid,
    (inferInstance : GCDMonoid ℤ) with
    normalize_gcd := fun _ _ => normalize_coe_nat _
    normalize_lcm := fun _ _ => normalize_coe_nat _ }

Integers as a Normalized GCD Monoid

Informal description

The integers $\mathbb{Z}$ form a normalized GCD monoid, meaning they have a well-defined greatest common divisor operation and a normalization function that maps each integer to its non-negative counterpart.

Int.coe_gcd theorem

(i j : ℤ) : ↑(Int.gcd i j) = GCDMonoid.gcd i j

Full source

theorem coe_gcd (i j : ℤ) : ↑(Int.gcd i j) = GCDMonoid.gcd i j :=
  rfl

Embedding of Integer GCD into GCD Monoid Structure

Informal description

For any integers $i$ and $j$, the canonical embedding of their greatest common divisor $\gcd(i, j)$ (computed via the integer-specific $\gcd$ operation) is equal to the greatest common divisor of $i$ and $j$ in the general GCD monoid structure on $\mathbb{Z}$.

Int.coe_lcm theorem

(i j : ℤ) : ↑(Int.lcm i j) = GCDMonoid.lcm i j

Full source

theorem coe_lcm (i j : ℤ) : ↑(Int.lcm i j) = GCDMonoid.lcm i j :=
  rfl

Embedding of Integer LCM into GCD Monoid Structure

Informal description

For any integers $i$ and $j$, the canonical embedding of their least common multiple $\mathrm{lcm}(i, j)$ (computed via the integer-specific $\mathrm{lcm}$ operation) is equal to the least common multiple of $i$ and $j$ in the general GCD monoid structure on $\mathbb{Z}$.

Int.natAbs_gcd theorem

(i j : ℤ) : natAbs (GCDMonoid.gcd i j) = Int.gcd i j

Full source

theorem natAbs_gcd (i j : ℤ) : natAbs (GCDMonoid.gcd i j) = Int.gcd i j :=
  rfl

Absolute Value of GCD in Integers Equals Integer GCD

Informal description

For any integers $i$ and $j$, the natural number obtained by taking the absolute value of their greatest common divisor (as elements of the GCD monoid $\mathbb{Z}$) is equal to the greatest common divisor of $i$ and $j$ in the integers, i.e., $\mathrm{natAbs}(\gcd(i, j)) = \gcd(i, j)$.

Int.natAbs_lcm theorem

(i j : ℤ) : natAbs (GCDMonoid.lcm i j) = Int.lcm i j

Full source

theorem natAbs_lcm (i j : ℤ) : natAbs (GCDMonoid.lcm i j) = Int.lcm i j :=
  rfl

Absolute Value of LCM in Integers Equals Integer LCM

Informal description

For any integers $i$ and $j$, the natural number obtained by taking the absolute value of their least common multiple (as elements of the GCD monoid $\mathbb{Z}$) is equal to the least common multiple of $i$ and $j$ in the integers, i.e., $\mathrm{natAbs}(\mathrm{lcm}(i, j)) = \mathrm{lcm}(i, j)$.

Int.exists_unit_of_abs theorem

(a : ℤ) : ∃ (u : ℤ) (_ : IsUnit u), (Int.natAbs a : ℤ) = u * a

Full source

theorem exists_unit_of_abs (a : ℤ) : ∃ (u : ℤ) (_ : IsUnit u), (Int.natAbs a : ℤ) = u * a := by
  rcases natAbs_eq a with h | h
  · use 1, isUnit_one
    rw [← h, one_mul]
  · use -1, isUnit_one.neg
    rw [← neg_eq_iff_eq_neg.mpr h]
    simp only [neg_mul, one_mul]

Existence of Unit Relating Absolute Value to Integer Multiplication

Informal description

For any integer $a$, there exists a unit $u$ in $\mathbb{Z}$ (i.e., $u = \pm 1$) such that the natural absolute value of $a$ (interpreted as an integer) equals $u \cdot a$, i.e., $|a| = u \cdot a$.

Int.gcd_eq_natAbs theorem

{a b : ℤ} : Int.gcd a b = Nat.gcd a.natAbs b.natAbs

Full source

theorem gcd_eq_natAbs {a b : ℤ} : Int.gcd a b = Nat.gcd a.natAbs b.natAbs :=
  rfl

$\gcd(a, b) = \gcd(|a|, |b|)$ for integers $a, b$

Informal description

For any integers $a$ and $b$, the greatest common divisor of $a$ and $b$ is equal to the greatest common divisor of their absolute values (as natural numbers), i.e., $\gcd(a, b) = \gcd(|a|, |b|)$.

associatesIntEquivNat definition

: Associates ℤ ≃ ℕ

Full source

/-- Maps an associate class of integers consisting of `-n, n` to `n : ℕ` -/
def associatesIntEquivNat : AssociatesAssociates ℤ ≃ ℕ := by
  refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
  · refine Associates.forall_associated.2 fun a ↦ ?_
    refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
    simp [Int.abs_eq_normalize, normalize_apply]
  · dsimp only [Associates.out_mk]
    rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]

Equivalence between associate classes of integers and natural numbers via absolute value

Informal description

The equivalence `associatesIntEquivNat` maps an associate class of integers (consisting of `-n` and `n`) to its natural absolute value `n : ℕ`. Specifically, it defines a bijection between the type of associate classes of integers and the natural numbers, where each associate class `[a]` is mapped to `|a|` (the natural absolute value of any representative of the class).

Int.associated_natAbs theorem

(k : ℤ) : Associated k k.natAbs

Full source

theorem Int.associated_natAbs (k : ℤ) : Associated k k.natAbs :=
  associated_of_dvd_dvd (Int.dvd_natCast.mpr dvd_rfl) (Int.natAbs_dvd.mpr dvd_rfl)

Integer Associated with its Natural Absolute Value

Informal description

For any integer $k$, the element $k$ is associated with its absolute value as a natural number, i.e., $k \sim |k|$ in the ring of integers $\mathbb{Z}$.

Int.associated_iff_natAbs theorem

{a b : ℤ} : Associated a b ↔ a.natAbs = b.natAbs

Full source

theorem Int.associated_iff_natAbs {a b : ℤ} : AssociatedAssociated a b ↔ a.natAbs = b.natAbs := by
  rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs,
    dvd_dvd_iff_associated]
  exact associated_iff_eq

Characterization of Integer Association via Natural Absolute Value Equality

Informal description

For any integers $a$ and $b$, $a$ is associated with $b$ (i.e., $a$ and $b$ differ by multiplication by a unit) if and only if their natural absolute values are equal: $|a| = |b|$.

Int.associated_iff theorem

{a b : ℤ} : Associated a b ↔ a = b ∨ a = -b

Full source

theorem Int.associated_iff {a b : ℤ} : AssociatedAssociated a b ↔ a = b ∨ a = -b := by
  rw [Int.associated_iff_natAbs]
  exact Int.natAbs_eq_natAbs_iff

Characterization of Integer Association via Equality or Negation

Informal description

For any integers $a$ and $b$, $a$ is associated with $b$ if and only if $a = b$ or $a = -b$.

Mathlib.Algebra.GCDMonoid.Nat

Main statements

Tags