Documentation

Mathlib.Algebra.GCDMonoid.Nat

ℕ and ℤ are normalized GCD monoids. #

Main statements #

Tags #

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

is a gcd_monoid.

Equations
    theorem gcd_eq_nat_gcd (m n : ) :
    gcd m n = m.gcd n
    theorem lcm_eq_nat_lcm (m n : ) :
    lcm m n = m.lcm n
    theorem Int.normUnit_eq (z : ) :
    normUnit z = if 0 z then 1 else -1
    theorem Int.normalize_of_nonneg {z : } (h : 0 z) :
    theorem Int.normalize_of_nonpos {z : } (h : z 0) :
    theorem Int.normalize_coe_nat (n : ) :
    normalize n = n
    theorem Int.eq_of_associated_of_nonneg {a b : } (h : Associated a b) (ha : 0 a) (hb : 0 b) :
    a = b
    theorem Int.coe_gcd (i j : ) :
    (i.gcd j) = GCDMonoid.gcd i j
    theorem Int.coe_lcm (i j : ) :
    (i.lcm j) = GCDMonoid.lcm i j
    theorem Int.natAbs_gcd (i j : ) :
    theorem Int.natAbs_lcm (i j : ) :
    theorem Int.gcd_eq_natAbs {a b : } :

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

    Equations
      Instances For
        theorem Int.associated_iff {a b : } :
        Associated a b a = b a = -b