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 : ℕ) :

@[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 < m → P (n % m) m → P m n) :

P m n

def nat.lcm (m n : ℕ) :

Equations

def nat.coprime (m n : ℕ) :

Prop

Equations