Definition and lemmas for gcd and lcm over Int

gcd

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

Computes the greatest common divisor of two integers, as a Nat.

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

lcm

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

Computes the least common multiple of two integers, as a Nat.

Equations

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

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

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

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

@[simp]

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