@[extern lean_nat_gcd]

def Nat.gcd (m : Nat) (n : Nat) : Nat

Equations

• Nat.gcd m n = if m = 0 then n else Nat.gcd (n % m) m

@[simp]

theorem Nat.gcd_zero_left (y : Nat) : Nat.gcd 0 y = y

theorem Nat.gcd_succ (x : Nat) (y : Nat) : Nat.gcd (Nat.succ x) y = Nat.gcd (y % Nat.succ x) (Nat.succ x)

@[simp]

theorem Nat.gcd_one_left (n : Nat) : Nat.gcd 1 n = 1

@[simp]

theorem Nat.gcd_zero_right (n : Nat) : Nat.gcd n 0 = n

@[simp]

theorem Nat.gcd_self (n : Nat) : Nat.gcd n n = n

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

theorem Nat.gcd.induction {P : Nat → Nat → Prop} (m : Nat) (n : Nat) (H0 : ∀ (n : Nat), P 0 n) (H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n) : P m n

theorem Nat.gcd_dvd (m : Nat) (n : Nat) : Nat.gcd m n ∣ m ∧ Nat.gcd m n ∣ n

theorem Nat.gcd_dvd_left (m : Nat) (n : Nat) : Nat.gcd m n ∣ m

theorem Nat.gcd_dvd_right (m : Nat) (n : Nat) : Nat.gcd m n ∣ n

theorem Nat.gcd_le_left {m : Nat} (n : Nat) (h : 0 < m) : Nat.gcd m n ≤ m

theorem Nat.gcd_le_right {m : Nat} (n : Nat) (h : 0 < n) : Nat.gcd m n ≤ n

theorem Nat.dvd_gcd {k : Nat} {m : Nat} {n : Nat} : k ∣ m → k ∣ n → k ∣ Nat.gcd m n