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
  • One or more equations did not get rendered due to their size.
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
Equations
  • One or more equations did not get rendered due to their size.
theorem Int.normUnit_eq (z : ) :
normUnit z = if 0 z then 1 else -1
theorem Int.normalize_of_nonneg {z : } (h : 0 z) :
normalize z = z
theorem Int.normalize_of_nonpos {z : } (h : z 0) :
normalize z = -z
theorem Int.normalize_coe_nat (n : ) :
normalize n = n
theorem Int.abs_eq_normalize (z : ) :
|z| = normalize z
theorem Int.nonneg_of_normalize_eq_self {z : } (hz : normalize z = z) :
0 z
theorem Int.nonneg_iff_normalize_eq_self (z : ) :
normalize z = z 0 z
theorem Int.eq_of_associated_of_nonneg {a : } {b : } (h : Associated a b) (ha : 0 a) (hb : 0 b) :
a = b
Equations
  • One or more equations did not get rendered due to their size.
theorem Int.coe_gcd (i : ) (j : ) :
(i.gcd j) = gcd i j
theorem Int.coe_lcm (i : ) (j : ) :
(i.lcm j) = lcm i j
theorem Int.natAbs_gcd (i : ) (j : ) :
(gcd i j).natAbs = i.gcd j
theorem Int.natAbs_lcm (i : ) (j : ) :
(lcm i j).natAbs = i.lcm j
theorem Int.exists_unit_of_abs (a : ) :
∃ (u : ), ∃ (x : IsUnit u), a.natAbs = u * a
theorem Int.gcd_eq_natAbs {a : } {b : } :
a.gcd b = a.natAbs.gcd b.natAbs

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
    theorem Int.associated_natAbs (k : ) :
    Associated k k.natAbs
    theorem Int.associated_iff_natAbs {a : } {b : } :
    Associated a b a.natAbs = b.natAbs
    theorem Int.associated_iff {a : } {b : } :
    Associated a b a = b a = -b