ℕ and ℤ are normalized GCD monoids.

Main statements

• ℕ is a GCDMonoid
• ℕ is a NormalizedGCDMonoid
• ℤ is a NormalizationMonoid
• ℤ is a GCDMonoid
• ℤ is a NormalizedGCDMonoid

Tags

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

instance instGCDMonoidNat : GCDMonoid ℕ

ℕ 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

instance instNormalizedGCDMonoidNat : NormalizedGCDMonoid ℕ

Equations

• instNormalizedGCDMonoidNat = let __src := inferInstance; let __src_1 := inferInstance; NormalizedGCDMonoid.mk instNormalizedGCDMonoidNat.proof_1 instNormalizedGCDMonoidNat.proof_2

instance Int.normalizationMonoid : NormalizationMonoid ℤ

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

instance Int.instGCDMonoid : GCDMonoid ℤ

Equations

• One or more equations did not get rendered due to their size.

instance Int.instNormalizedGCDMonoid : NormalizedGCDMonoid ℤ

Equations

• Int.instNormalizedGCDMonoid = let __src := Int.normalizationMonoid; let __src_1 := inferInstance; NormalizedGCDMonoid.mk Int.instNormalizedGCDMonoid.proof_1 Int.instNormalizedGCDMonoid.proof_2

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 : ℤ) (_ : IsUnit u), ↑a.natAbs = u * a

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

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.

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