# Documentation

## Init.Data.Int.Gcd

Definition and lemmas for gcd and lcm over Int

## gcd #

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

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

Equations
• m.gcd n = m.natAbs.gcd n.natAbs
Instances For
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) :

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

Equations
• m.lcm n = m.natAbs.lcm n.natAbs
Instances For
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