mathlib3 documentation

core / init.data.nat.gcd

Definitions and properties of gcd, lcm, and coprime #

gcd

source
def nat.gcd  :
ℕ → ℕ → ℕ
Equations
source
@[simp]
theorem nat.gcd_zero_left (x : ℕ) :
0.gcd x = x
source
@[simp]
theorem nat.gcd_succ (x y : ℕ) :
x.succ.gcd y = (y % x.succ).gcd x.succ
source
@[simp]
theorem nat.gcd_one_left (n : ℕ) :
1.gcd n = 1
source
theorem nat.gcd_def (x y : ℕ) :
x.gcd y = ite (x = 0) y ((y % x).gcd x)
source
@[simp]
theorem nat.gcd_self (n : ℕ) :
n.gcd n = n
source
@[simp]
theorem nat.gcd_zero_right (n : ℕ) :
n.gcd 0 = n
source
theorem nat.gcd_rec (m n : ℕ) :
m.gcd n = (n % m).gcd m
source
theorem nat.gcd.induction {P : ℕ → ℕ → Prop} (m n : ℕ) (H0 : ∀ (n : ℕ), P 0 n) (H1 : ∀ (m n : ℕ), 0 < m → P (n % m) m → P m n) :
P m n
source
def nat.lcm (m n : ℕ) :
ℕ
Equations
Instances for nat.lcm
source
@[reducible]
def nat.coprime (m n : ℕ) :
Prop
Equations