@[irreducible, extern lean_nat_gcd]

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

Computes the greatest common divisor of two natural numbers.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

The GCD of two natural numbers is the largest natural number that divides both arguments. In particular, the GCD of a number and 0 is the number itself:

example : Nat.gcd 10 15 = 5 := rfl
example : Nat.gcd 0 5 = 5 := rfl
example : Nat.gcd 7 0 = 7 := rfl

Equations

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

instance Nat.instLawfulIdentityGcdOfNat : Std.LawfulIdentity Nat.gcd 0

Equations

• Nat.instLawfulIdentityGcdOfNat = ⋯

@[simp]

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

instance Nat.instIdempotentOpGcd : Std.IdempotentOp Nat.gcd

Equations

• Nat.instIdempotentOpGcd = ⋯

theorem Nat.gcd_rec (m : Nat) (n : Nat) : m.gcd n = (n % m).gcd 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) : m.gcd n ∣ m ∧ m.gcd n ∣ n

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

theorem Nat.gcd_dvd_right (m : Nat) (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 : Nat} {m : Nat} {n : Nat} : k ∣ m → k ∣ n → k ∣ m.gcd n

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

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

instance Nat.instCommutativeGcd : Std.Commutative Nat.gcd

Equations

• Nat.instCommutativeGcd = ⋯

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

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

theorem Nat.gcd_assoc (m : Nat) (n : Nat) (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 : Nat) (n : Nat) (k : Nat) : (m * n).gcd (m * k) = m * n.gcd k

theorem Nat.gcd_mul_right (m : Nat) (n : Nat) (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 : Nat} {n : Nat} (H : m.gcd n = 0) : m = 0

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

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

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

theorem Nat.gcd_div {m : Nat} {n : Nat} {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 : Nat} {k : Nat} (n : Nat) (H : m ∣ k) : m.gcd n ∣ k.gcd n

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Nat.gcd_eq_iff {g : Nat} {a : Nat} {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.prod_dvd_and_dvd_of_dvd_prod {k : Nat} {m : Nat} {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 = if h0 : k.gcd m = 0 then ⟨(⟨0, ⋯⟩, ⟨n, ⋯⟩), ⋯⟩ else let_fun hd := ⋯; ⟨(⟨k.gcd m, ⋯⟩, ⟨k / k.gcd m, ⋯⟩), ⋯⟩

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