Documentation

Mathlib.Algebra.GCDMonoid.Nat

ℕ and ℤ are normalized GCD monoids. #

Main statements #

Tags #

natural numbers, integers, normalization monoid, gcd monoid, greatest common divisor

source
@[implicit_reducible]
instance instGCDMonoidNat :
GCDMonoid ℕ

ℕ is a GCDMonoid.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem gcd_eq_nat_gcd (m n : ℕ) :
gcd m n = m.gcd n
source
theorem lcm_eq_nat_lcm (m n : ℕ) :
lcm m n = m.lcm n
source
@[implicit_reducible]
instance instStrongNormalizedGCDMonoidNat :
StrongNormalizedGCDMonoid ℕ
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
instance Int.strongNormalizationMonoid :
StrongNormalizationMonoid ℤ
Equations
  • One or more equations did not get rendered due to their size.
source
@[deprecated Int.strongNormalizationMonoid (since := "2026-07-08")]
def Int.normalizationMonoid :
StrongNormalizationMonoid ℤ

Alias of Int.strongNormalizationMonoid.

Equations
Instances For
    source
    theorem Int.normUnit_eq (z : ℤ) :
    normUnit z = if 0 ≤ z then 1 else -1
    source
    theorem Int.normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) :
    normalize z = z
    source
    theorem Int.normalize_of_nonpos {z : ℤ} (h : z ≤ 0) :
    normalize z = -z
    source
    theorem Int.normalize_coe_nat (n : ℕ) :
    normalize ↑n = ↑n
    source
    theorem Int.abs_eq_normalize (z : ℤ) :
    |z| = normalize z
    source
    theorem Int.nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) :
    0 ≤ z
    source
    theorem Int.nonneg_iff_normalize_eq_self (z : ℤ) :
    normalize z = z ↔ 0 ≤ z
    source
    theorem Int.eq_of_associated_of_nonneg {a b : ℤ} (h : Associated a b) (ha : 0 ≤ a) (hb : 0 ≤ b) :
    a = b
    source
    @[implicit_reducible]
    instance Int.instGCDMonoid :
    GCDMonoid ℤ
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    instance Int.instStrongNormalizedGCDMonoid :
    StrongNormalizedGCDMonoid ℤ
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Int.coe_gcd (i j : ℤ) :
    ↑(i.gcd j) = GCDMonoid.gcd i j
    source
    theorem Int.coe_lcm (i j : ℤ) :
    ↑(i.lcm j) = GCDMonoid.lcm i j
    source
    theorem Int.natAbs_gcd (i j : ℤ) :
    (GCDMonoid.gcd i j).natAbs = i.gcd j
    source
    theorem Int.natAbs_lcm (i j : ℤ) :
    (GCDMonoid.lcm i j).natAbs = i.lcm j
    source
    theorem Int.gcd_nonneg (i j : ℤ) :
    0 ≤ GCDMonoid.gcd i j
    source
    theorem Int.lcm_nonneg (i j : ℤ) :
    0 ≤ GCDMonoid.lcm i j
    source
    theorem Int.exists_unit_of_abs (a : ℤ) :
    ∃ (u : ℤ), ∃ (x : IsUnit u), ↑a.natAbs = u * a
    source
    theorem Int.gcd_eq_natAbs {a b : ℤ} :
    a.gcd b = a.natAbs.gcd b.natAbs
    source
    def associatesIntEquivNat :
    Associates ℤ ≃ ℕ

    Maps an associate class of integers consisting of -n, n to n : ℕ

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Int.associated_natAbs (k : ℤ) :
      Associated k ↑k.natAbs
      source
      theorem Int.associated_iff_natAbs {a b : ℤ} :
      Associated a b ↔ a.natAbs = b.natAbs
      source
      theorem Int.associated_iff {a b : ℤ} :
      Associated a b ↔ a = b ∨ a = -b