Results about Int.gcd.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• Int.lcm m n = Nat.lcm (Int.natAbs m) (Int.natAbs n)

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

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

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

@[simp]

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