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 : ) (H0 : ∀ (n : ), P 0 n) (H1 : ∀ (m n : ), 0 < mP (n % m) mP m n) :
P m n
def nat.lcm (m n : ) :
Equations
Instances for nat.lcm
@[reducible]
def nat.coprime (m n : ) :
Prop
Equations