Documentation

Init.Data.Nat.Gcd

@[irreducible, extern lean_nat_gcd]
def Nat.gcd (m : Nat) (n : 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
Instances For
@[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)
@[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
Equations
@[simp]
theorem Nat.gcd_self (n : Nat) :
n.gcd n = n
Equations
theorem Nat.gcd_rec (m : Nat) (n : Nat) :
m.gcd n = (n % m).gcd m
theorem Nat.gcd.induction {P : } (m : Nat) (n : Nat) (H0 : ∀ (n : Nat), P 0 n) (H1 : ∀ (m n : Nat), 0 < mP (n % m) mP 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 mk nk 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
Equations
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 0m.gcd n 0
theorem Nat.gcd_ne_zero_right {n : Nat} {m : Nat} :
n 0m.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 ac bc 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
• = if h0 : k.gcd m = 0 then (0, , n, ), else let_fun hd := ; (k.gcd m, , k / k.gcd m, ),
Instances For
theorem Nat.gcd_mul_dvd_mul_gcd (k : Nat) (m : Nat) (n : Nat) :
k.gcd (m * n) k.gcd m * k.gcd n