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
def nat.coprime (m n : ) :
Prop

Equations