@[irreducible, extern lean_nat_gcd]

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

Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the largest natural number that evenly divides both.

In particular, the GCD of a number and 0 is the number itself.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here is the logical model.

Examples:

• Nat.gcd 10 15 = 5
• Nat.gcd 0 5 = 5
• Nat.gcd 7 0 = 7

Equations

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

Instances For

• Nat.instCommutativeGcd
• Nat.instIdempotentOpGcd
• Nat.instLawfulIdentityGcdOfNat

@[simp]

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

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

theorem Nat.gcd_add_one (x y : Nat) : (x + 1).gcd y = (y % (x + 1)).gcd (x + 1)

theorem Nat.gcd_def (x y : Nat) : x.gcd y = if x = 0 then y else (y % x).gcd x

@[simp]

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

@[simp]

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

instance Nat.instLawfulIdentityGcdOfNat : Std.LawfulIdentity gcd 0

@[simp]

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

instance Nat.instIdempotentOpGcd : Std.IdempotentOp gcd

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

theorem Nat.gcd.induction {P : Nat → Nat → Prop} (m 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 n : Nat) : m.gcd n ∣ m ∧ m.gcd n ∣ n

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

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

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

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

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

theorem Nat.dvd_gcd_iff {k : Nat} {m n : Nat} : k ∣ m.gcd n ↔ k ∣ m ∧ k ∣ n

theorem Nat.gcd_comm (m n : Nat) : m.gcd n = n.gcd m

instance Nat.instCommutativeGcd : Std.Commutative gcd

theorem Nat.gcd_eq_left_iff_dvd {m n : Nat} : m.gcd n = m ↔ m ∣ n

theorem Nat.gcd_eq_right_iff_dvd {n m : Nat} : n.gcd m = m ↔ m ∣ n

theorem Nat.gcd_assoc (m n k : Nat) : (m.gcd n).gcd k = m.gcd (n.gcd k)

@[simp]

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

theorem Nat.gcd_mul_left (m n k : Nat) : (m * n).gcd (m * k) = m * n.gcd k

theorem Nat.gcd_mul_right (m n k : Nat) : (m * n).gcd (k * n) = m.gcd k * n

theorem Nat.gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < m.gcd n

theorem Nat.gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < m.gcd n

theorem Nat.div_gcd_pos_of_pos_left {a : Nat} (b : Nat) (h : 0 < a) : 0 < a / a.gcd b

theorem Nat.div_gcd_pos_of_pos_right {b : Nat} (a : Nat) (h : 0 < b) : 0 < b / a.gcd b

theorem Nat.eq_zero_of_gcd_eq_zero_left {m n : Nat} (H : m.gcd n = 0) : m = 0

theorem Nat.eq_zero_of_gcd_eq_zero_right {m n : Nat} (H : m.gcd n = 0) : n = 0

theorem Nat.gcd_ne_zero_left {m n : Nat} : m ≠ 0 → m.gcd n ≠ 0

theorem Nat.gcd_ne_zero_right {n m : Nat} : n ≠ 0 → m.gcd n ≠ 0

theorem Nat.gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) : (m / k).gcd (n / k) = m.gcd n / k

theorem Nat.gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : m.gcd n ∣ k.gcd n

theorem Nat.gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : n.gcd m ∣ n.gcd k

theorem Nat.gcd_dvd_gcd_mul_left_left (m n k : Nat) : m.gcd n ∣ (k * m).gcd n

@[deprecated Nat.gcd_dvd_gcd_mul_left_left (since := "2025-04-01")]

theorem Nat.gcd_dvd_gcd_mul_left (m n k : Nat) : m.gcd n ∣ (k * m).gcd n

theorem Nat.gcd_dvd_gcd_mul_right_left (m n k : Nat) : m.gcd n ∣ (m * k).gcd n

@[deprecated Nat.gcd_dvd_gcd_mul_right_left (since := "2025-04-01")]

theorem Nat.gcd_dvd_gcd_mul_right (m n k : Nat) : m.gcd n ∣ (m * k).gcd n

theorem Nat.gcd_dvd_gcd_mul_left_right (m n k : Nat) : m.gcd n ∣ m.gcd (k * n)

theorem Nat.gcd_dvd_gcd_mul_right_right (m n k : Nat) : m.gcd n ∣ m.gcd (n * k)

theorem Nat.gcd_eq_left {m n : Nat} (H : m ∣ n) : m.gcd n = m

theorem Nat.gcd_eq_right {m n : Nat} (H : n ∣ m) : m.gcd n = n

theorem Nat.gcd_right_eq_iff {m n n' : Nat} : m.gcd n = m.gcd n' ↔ ∀ (k : Nat), k ∣ m → (k ∣ n ↔ k ∣ n')

theorem Nat.gcd_left_eq_iff {m m' n : Nat} : m.gcd n = m'.gcd n ↔ ∀ (k : Nat), k ∣ n → (k ∣ m ↔ k ∣ m')

@[simp]

theorem Nat.gcd_mul_left_left (m n : Nat) : (m * n).gcd n = n

@[simp]

theorem Nat.gcd_mul_left_right (m n : Nat) : n.gcd (m * n) = n

@[simp]

theorem Nat.gcd_mul_right_left (m n : Nat) : (n * m).gcd n = n

@[simp]

theorem Nat.gcd_mul_right_right (m n : Nat) : n.gcd (n * m) = n

@[simp]

theorem Nat.gcd_gcd_self_right_left (m n : Nat) : m.gcd (m.gcd n) = m.gcd n

@[simp]

theorem Nat.gcd_gcd_self_right_right (m n : Nat) : m.gcd (n.gcd m) = n.gcd m

@[simp]

theorem Nat.gcd_gcd_self_left_right (m n : Nat) : (n.gcd m).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_gcd_self_left_left (m n : Nat) : (m.gcd n).gcd m = m.gcd n

@[simp]

theorem Nat.gcd_add_mul_right_right (m n k : Nat) : m.gcd (n + k * m) = m.gcd n

@[deprecated Nat.gcd_add_mul_right_right (since := "2025-03-31")]

theorem Nat.gcd_add_mul_self (m n k : Nat) : m.gcd (n + k * m) = m.gcd n

@[simp]

theorem Nat.gcd_add_mul_left_right (m n k : Nat) : m.gcd (n + m * k) = m.gcd n

@[simp]

theorem Nat.gcd_mul_right_add_right (m n k : Nat) : m.gcd (k * m + n) = m.gcd n

@[simp]

theorem Nat.gcd_mul_left_add_right (m n k : Nat) : m.gcd (m * k + n) = m.gcd n

@[simp]

theorem Nat.gcd_add_mul_right_left (m n k : Nat) : (n + k * m).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_add_mul_left_left (m n k : Nat) : (n + m * k).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_mul_right_add_left (m n k : Nat) : (k * m + n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_mul_left_add_left (m n k : Nat) : (m * k + n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_add_self_right (m n : Nat) : m.gcd (n + m) = m.gcd n

@[simp]

theorem Nat.gcd_self_add_right (m n : Nat) : m.gcd (m + n) = m.gcd n

@[simp]

theorem Nat.gcd_add_self_left (m n : Nat) : (n + m).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_self_add_left (m n : Nat) : (m + n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_add_left_left_of_dvd {m k : Nat} (n : Nat) : m ∣ k → (k + n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_add_right_left_of_dvd {m k : Nat} (n : Nat) : m ∣ k → (n + k).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_add_left_right_of_dvd {n k : Nat} (m : Nat) : n ∣ k → n.gcd (k + m) = n.gcd m

@[simp]

theorem Nat.gcd_add_right_right_of_dvd {n k : Nat} (m : Nat) : n ∣ k → n.gcd (m + k) = n.gcd m

@[simp]

theorem Nat.gcd_sub_mul_right_right {m n k : Nat} (h : k * m ≤ n) : m.gcd (n - k * m) = m.gcd n

@[simp]

theorem Nat.gcd_sub_mul_left_right {m n k : Nat} (h : m * k ≤ n) : m.gcd (n - m * k) = m.gcd n

@[simp]

theorem Nat.gcd_mul_right_sub_right {m n k : Nat} (h : n ≤ k * m) : m.gcd (k * m - n) = m.gcd n

@[simp]

theorem Nat.gcd_mul_left_sub_right {m n k : Nat} (h : n ≤ m * k) : m.gcd (m * k - n) = m.gcd n

@[simp]

theorem Nat.gcd_sub_mul_right_left {m n k : Nat} (h : k * m ≤ n) : (n - k * m).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_sub_mul_left_left {m n k : Nat} (h : m * k ≤ n) : (n - m * k).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_mul_right_sub_left {m n k : Nat} (h : n ≤ k * m) : (k * m - n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_mul_left_sub_left {m n k : Nat} (h : n ≤ m * k) : (m * k - n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_sub_self_right {m n : Nat} (h : m ≤ n) : m.gcd (n - m) = m.gcd n

@[simp]

theorem Nat.gcd_self_sub_right {m n : Nat} (h : n ≤ m) : m.gcd (m - n) = m.gcd n

@[simp]

theorem Nat.gcd_sub_self_left {m n : Nat} (h : m ≤ n) : (n - m).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_self_sub_left {m n : Nat} (h : n ≤ m) : (m - n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_sub_left_left_of_dvd {n k : Nat} (m : Nat) (h : n ≤ k) : m ∣ k → (k - n).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_sub_right_left_of_dvd {n k : Nat} (m : Nat) (h : k ≤ n) : m ∣ k → (n - k).gcd m = n.gcd m

@[simp]

theorem Nat.gcd_sub_left_right_of_dvd {m k : Nat} (n : Nat) (h : m ≤ k) : n ∣ k → n.gcd (k - m) = n.gcd m

@[simp]

theorem Nat.gcd_sub_right_right_of_dvd {m k : Nat} (n : Nat) (h : k ≤ m) : n ∣ k → n.gcd (m - k) = n.gcd m

@[simp]

theorem Nat.gcd_eq_zero_iff {i j : Nat} : i.gcd j = 0 ↔ i = 0 ∧ j = 0

theorem Nat.gcd_eq_iff {g a b : Nat} : a.gcd b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g

Characterization of the value of Nat.gcd.

def Nat.dvdProdDvdOfDvdProd {k m n : Nat} (h : k ∣ m * n) : { d : { m' : Nat // m' ∣ m } × { n' : Nat // n' ∣ n } // k = d.fst.val * d.snd.val }

Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

Equations

• Nat.dvdProdDvdOfDvdProd h = if h0 : k.gcd m = 0 then ⟨(⟨0, ⋯⟩, ⟨n, ⋯⟩), ⋯⟩ else let_fun hd := ⋯; ⟨(⟨k.gcd m, ⋯⟩, ⟨k / k.gcd m, ⋯⟩), ⋯⟩

@[deprecated Nat.dvdProdDvdOfDvdProd (since := "2025-04-01")]

def Nat.prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) : { d : { m' : Nat // m' ∣ m } × { n' : Nat // n' ∣ n } // k = d.fst.val * d.snd.val }

Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

Equations

• Nat.prod_dvd_and_dvd_of_dvd_prod H = Nat.dvdProdDvdOfDvdProd H

theorem Nat.dvd_mul {k m n : Nat} : k ∣ m * n ↔ ∃ (k₁ : Nat), ∃ (k₂ : Nat), k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k

theorem Nat.gcd_mul_dvd_mul_gcd (k m n : Nat) : k.gcd (m * n) ∣ k.gcd m * k.gcd n

theorem Nat.dvd_gcd_mul_iff_dvd_mul {k n m : Nat} : k ∣ k.gcd n * m ↔ k ∣ n * m

theorem Nat.dvd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ n * k.gcd m ↔ k ∣ n * m

theorem Nat.dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ k.gcd n * k.gcd m ↔ k ∣ n * m

theorem Nat.gcd_eq_one_iff {m n : Nat} : m.gcd n = 1 ↔ ∀ (c : Nat), c ∣ m → c ∣ n → c = 1

theorem Nat.gcd_mul_right_right_of_gcd_eq_one {n m k : Nat} : n.gcd m = 1 → n.gcd (m * k) = n.gcd k

theorem Nat.gcd_mul_left_right_of_gcd_eq_one {n m k : Nat} (h : n.gcd m = 1) : n.gcd (k * m) = n.gcd k

theorem Nat.gcd_mul_right_left_of_gcd_eq_one {n m k : Nat} (h : n.gcd m = 1) : (n * k).gcd m = k.gcd m

theorem Nat.gcd_mul_left_left_of_gcd_eq_one {n m k : Nat} (h : n.gcd m = 1) : (k * n).gcd m = k.gcd m

theorem Nat.gcd_pow_left_of_gcd_eq_one {k n m : Nat} (h : n.gcd m = 1) : (n ^ k).gcd m = 1

theorem Nat.gcd_pow_right_of_gcd_eq_one {k n m : Nat} (h : n.gcd m = 1) : n.gcd (m ^ k) = 1

theorem Nat.pow_gcd_pow_of_gcd_eq_one {k l n m : Nat} (h : n.gcd m = 1) : (n ^ k).gcd (m ^ l) = 1

theorem Nat.gcd_div_gcd_div_gcd_of_pos_left {n m : Nat} (h : 0 < n) : (n / n.gcd m).gcd (m / n.gcd m) = 1

theorem Nat.gcd_div_gcd_div_gcd_of_pos_right {n m : Nat} (h : 0 < m) : (n / n.gcd m).gcd (m / n.gcd m) = 1

theorem Nat.pow_gcd_pow {k n m : Nat} : (n ^ k).gcd (m ^ k) = n.gcd m ^ k

theorem Nat.pow_dvd_pow_iff {a b n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b