Definition and lemmas for gcd and lcm over Int

Future work

Most of the material about Nat.gcd and Nat.lcm from Init.Data.Nat.Gcd and Init.Data.Nat.Lcm has analogues for Int.gcd and Int.lcm that should be added to this file.

gcd

def Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is the largest natural number that evenly divides both. However, the GCD of a number and 0 is the number's absolute value.

This implementation uses Nat.gcd, which is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic.

Examples:

• Int.gcd 10 15 = 5
• Int.gcd 10 (-15) = 5
• Int.gcd (-6) (-9) = 3
• Int.gcd 0 5 = 5
• Int.gcd (-7) 0 = 7

Equations

• m.gcd n = m.natAbs.gcd n.natAbs

theorem Int.gcd_dvd_left {a b : Int} : ↑(a.gcd b) ∣ a

theorem Int.gcd_dvd_right {a b : Int} : ↑(a.gcd b) ∣ b

@[simp]

theorem Int.one_gcd {a : Int} : gcd 1 a = 1

@[simp]

theorem Int.gcd_one {a : Int} : a.gcd 1 = 1

@[simp]

theorem Int.neg_gcd {a b : Int} : (-a).gcd b = a.gcd b

@[simp]

theorem Int.gcd_neg {a b : Int} : a.gcd (-b) = a.gcd b

lcm

def Int.lcm (m n : Int) : Nat

Computes the least common multiple of two integers as a natural number. The LCM of two integers is the smallest natural number that's evenly divisible by the absolute values of both.

Examples:

• Int.lcm 9 6 = 18
• Int.lcm 9 (-6) = 18
• Int.lcm 9 3 = 9
• Int.lcm 9 (-3) = 9
• Int.lcm 0 3 = 0
• Int.lcm (-3) 0 = 0

Equations

• m.lcm n = m.natAbs.lcm n.natAbs

theorem Int.lcm_ne_zero {m n : Int} (hm : m ≠ 0) (hn : n ≠ 0) : m.lcm n ≠ 0

theorem Int.dvd_lcm_left {a b : Int} : a ∣ ↑(a.lcm b)

theorem Int.dvd_lcm_right {a b : Int} : b ∣ ↑(a.lcm b)

@[simp]

theorem Int.lcm_self {a : Int} : a.lcm a = a.natAbs