mathlib documentation

core.init.data.nat.gcd

def nat.gcd  :

Equations
@[simp]
theorem nat.gcd_zero_left (x : ) :
0.gcd x = x

@[simp]
theorem nat.gcd_succ (x y : ) :
x.succ.gcd y = (y % x.succ).gcd x.succ

@[simp]
theorem nat.gcd_one_left (n : ) :
1.gcd n = 1

theorem nat.gcd_def (x y : ) :
x.gcd y = ite (x = 0) y ((y % x).gcd x)

@[simp]
theorem nat.gcd_self (n : ) :
n.gcd n = n

@[simp]
theorem nat.gcd_zero_right (n : ) :
n.gcd 0 = n

theorem nat.gcd_rec (m n : ) :
m.gcd n = (n % m).gcd m

theorem nat.gcd.induction {P : → Prop} (m n : ) :
(∀ (n : ), P 0 n)(∀ (m n : ), 0 < mP (n % m) mP m n)P m n

def nat.lcm  :

Equations
def nat.coprime  :
→ Prop

Equations