Std.Data.Nat.Gcd

# Definitions and properties of gcd, lcm, and coprime#

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

The least common multiple of m and n, defined using gcd.

Equations
Instances For
@[reducible]
def Nat.Coprime (m : Nat) (n : Nat) :

m and n are coprime, or relatively prime, if their gcd is 1.

Equations
Instances For
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 mk nk Nat.gcd m n
theorem Nat.dvd_gcd_iff {k : Nat} {m : Nat} {n : Nat} :
k Nat.gcd m n k m k n
theorem Nat.gcd_comm (m : Nat) (n : Nat) :
Nat.gcd m n = Nat.gcd n m
theorem Nat.gcd_eq_left_iff_dvd {m : Nat} {n : Nat} :
m n Nat.gcd m n = m
theorem Nat.gcd_eq_right_iff_dvd {m : Nat} {n : Nat} :
m n Nat.gcd n m = m
theorem Nat.gcd_assoc (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd (Nat.gcd m n) k = Nat.gcd m (Nat.gcd n k)
@[simp]
theorem Nat.gcd_one_right (n : Nat) :
Nat.gcd n 1 = 1
theorem Nat.gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd (m * n) (m * k) = m * Nat.gcd n k
theorem Nat.gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd (m * n) (k * n) = Nat.gcd m k * n
theorem Nat.gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) :
0 < Nat.gcd m n
theorem Nat.gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) :
0 < Nat.gcd m n
theorem Nat.div_gcd_pos_of_pos_left {a : Nat} (b : Nat) (h : 0 < a) :
0 < a / Nat.gcd a b
theorem Nat.div_gcd_pos_of_pos_right {b : Nat} (a : Nat) (h : 0 < b) :
0 < b / Nat.gcd a b
theorem Nat.eq_zero_of_gcd_eq_zero_left {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
m = 0
theorem Nat.eq_zero_of_gcd_eq_zero_right {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
n = 0
theorem Nat.gcd_ne_zero_left {m : Nat} {n : Nat} :
m 0Nat.gcd m n 0
theorem Nat.gcd_ne_zero_right {n : Nat} {m : Nat} :
n 0Nat.gcd m n 0
theorem Nat.gcd_div {m : Nat} {n : Nat} {k : Nat} (H1 : k m) (H2 : k n) :
Nat.gcd (m / k) (n / k) = Nat.gcd m n / k
theorem Nat.gcd_dvd_gcd_of_dvd_left {m : Nat} {k : Nat} (n : Nat) (H : m k) :
theorem Nat.gcd_dvd_gcd_of_dvd_right {m : Nat} {k : Nat} (n : Nat) (H : m k) :
theorem Nat.gcd_dvd_gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd m n Nat.gcd (k * m) n
theorem Nat.gcd_dvd_gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd m n Nat.gcd (m * k) n
theorem Nat.gcd_dvd_gcd_mul_left_right (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd m n Nat.gcd m (k * n)
theorem Nat.gcd_dvd_gcd_mul_right_right (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd m n Nat.gcd m (n * k)
theorem Nat.gcd_eq_left {m : Nat} {n : Nat} (H : m n) :
Nat.gcd m n = m
theorem Nat.gcd_eq_right {m : Nat} {n : Nat} (H : n m) :
Nat.gcd m n = n
@[simp]
theorem Nat.gcd_mul_left_left (m : Nat) (n : Nat) :
Nat.gcd (m * n) n = n
@[simp]
theorem Nat.gcd_mul_left_right (m : Nat) (n : Nat) :
Nat.gcd n (m * n) = n
@[simp]
theorem Nat.gcd_mul_right_left (m : Nat) (n : Nat) :
Nat.gcd (n * m) n = n
@[simp]
theorem Nat.gcd_mul_right_right (m : Nat) (n : Nat) :
Nat.gcd n (n * m) = n
@[simp]
theorem Nat.gcd_gcd_self_right_left (m : Nat) (n : Nat) :
Nat.gcd m (Nat.gcd m n) = Nat.gcd m n
@[simp]
theorem Nat.gcd_gcd_self_right_right (m : Nat) (n : Nat) :
Nat.gcd m (Nat.gcd n m) = Nat.gcd n m
@[simp]
theorem Nat.gcd_gcd_self_left_right (m : Nat) (n : Nat) :
Nat.gcd (Nat.gcd n m) m = Nat.gcd n m
@[simp]
theorem Nat.gcd_gcd_self_left_left (m : Nat) (n : Nat) :
Nat.gcd (Nat.gcd m n) m = Nat.gcd m n
theorem Nat.gcd_add_mul_self (m : Nat) (n : Nat) (k : Nat) :
Nat.gcd m (n + k * m) = Nat.gcd m n
theorem Nat.gcd_eq_zero_iff {i : Nat} {j : Nat} :
Nat.gcd i j = 0 i = 0 j = 0
theorem Nat.gcd_eq_iff {g : Nat} (a : Nat) (b : Nat) :
Nat.gcd a b = g g a g b ∀ (c : Nat), c ac bc g

Characterization of the value of Nat.gcd.

### lcm#

theorem Nat.lcm_comm (m : Nat) (n : Nat) :
Nat.lcm m n = Nat.lcm n m
@[simp]
theorem Nat.lcm_zero_left (m : Nat) :
Nat.lcm 0 m = 0
@[simp]
theorem Nat.lcm_zero_right (m : Nat) :
Nat.lcm m 0 = 0
@[simp]
theorem Nat.lcm_one_left (m : Nat) :
Nat.lcm 1 m = m
@[simp]
theorem Nat.lcm_one_right (m : Nat) :
Nat.lcm m 1 = m
@[simp]
theorem Nat.lcm_self (m : Nat) :
Nat.lcm m m = m
theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) :
m Nat.lcm m n
theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) :
n Nat.lcm m n
theorem Nat.gcd_mul_lcm (m : Nat) (n : Nat) :
Nat.gcd m n * Nat.lcm m n = m * n
theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m k) (H2 : n k) :
Nat.lcm m n k
theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) :
Nat.lcm (Nat.lcm m n) k = Nat.lcm m (Nat.lcm n k)
theorem Nat.lcm_ne_zero {m : Nat} {n : Nat} (hm : m 0) (hn : n 0) :
Nat.lcm m n 0

### coprime#

See also nat.coprime_of_dvd and nat.coprime_of_dvd' to prove nat.Coprime m n.

instance Nat.instDecidableCoprime (m : Nat) (n : Nat) :
Equations
theorem Nat.coprime_iff_gcd_eq_one {m : Nat} {n : Nat} :
Nat.gcd m n = 1
theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} :
Nat.gcd m n = 1
theorem Nat.Coprime.symm {n : Nat} {m : Nat} :
theorem Nat.coprime_comm {n : Nat} {m : Nat} :
theorem Nat.Coprime.dvd_of_dvd_mul_right {k : Nat} {n : Nat} {m : Nat} (H1 : ) (H2 : k m * n) :
k m
theorem Nat.Coprime.dvd_of_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (H1 : ) (H2 : k m * n) :
k n
theorem Nat.Coprime.gcd_mul_left_cancel {k : Nat} {n : Nat} (m : Nat) (H : ) :
Nat.gcd (k * m) n = Nat.gcd m n
theorem Nat.Coprime.gcd_mul_right_cancel {k : Nat} {n : Nat} (m : Nat) (H : ) :
Nat.gcd (m * k) n = Nat.gcd m n
theorem Nat.Coprime.gcd_mul_left_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : ) :
Nat.gcd m (k * n) = Nat.gcd m n
theorem Nat.Coprime.gcd_mul_right_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : ) :
Nat.gcd m (n * k) = Nat.gcd m n
theorem Nat.coprime_div_gcd_div_gcd {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
Nat.Coprime (m / Nat.gcd m n) (n / Nat.gcd m n)
theorem Nat.not_coprime_of_dvd_of_dvd {d : Nat} {m : Nat} {n : Nat} (dgt1 : 1 < d) (Hm : d m) (Hn : d n) :
theorem Nat.exists_coprime {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
∃ (m' : Nat), ∃ (n' : Nat), Nat.Coprime m' n' m = m' * Nat.gcd m n n = n' * Nat.gcd m n
theorem Nat.exists_coprime' {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
∃ (g : Nat), ∃ (m' : Nat), ∃ (n' : Nat), 0 < g Nat.Coprime m' n' m = m' * g n = n' * g
theorem Nat.Coprime.mul {m : Nat} {k : Nat} {n : Nat} (H1 : ) (H2 : ) :
Nat.Coprime (m * n) k
theorem Nat.Coprime.mul_right {k : Nat} {m : Nat} {n : Nat} (H1 : ) (H2 : ) :
Nat.Coprime k (m * n)
theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m k) (H2 : ) :
theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n m) (H2 : ) :
theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : Nat.Coprime (k * m) n) :
theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime (m * k) n) :
theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime m (k * n)) :
theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : Nat.Coprime m (n * k)) :
theorem Nat.Coprime.coprime_div_left {m : Nat} {n : Nat} {a : Nat} (cmn : ) (dvd : a m) :
Nat.Coprime (m / a) n
theorem Nat.Coprime.coprime_div_right {m : Nat} {n : Nat} {a : Nat} (cmn : ) (dvd : a n) :
Nat.Coprime m (n / a)
theorem Nat.coprime_mul_iff_left {m : Nat} {n : Nat} {k : Nat} :
Nat.Coprime (m * n) k
theorem Nat.coprime_mul_iff_right {k : Nat} {m : Nat} {n : Nat} :
Nat.Coprime k (m * n)
theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : ) :
theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : ) :
theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : ) :
theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd {m : Nat} {n : Nat} {a : Nat} (hmn : ) (hm : m a) (hn : n a) :
m * n a
@[simp]
theorem Nat.coprime_zero_left (n : Nat) :
n = 1
@[simp]
theorem Nat.coprime_zero_right (n : Nat) :
n = 1
@[simp]
theorem Nat.coprime_self (n : Nat) :
n = 1
theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : ) :
Nat.Coprime (m ^ n) k
theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : ) :
Nat.Coprime k (m ^ n)
theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : ) :
Nat.Coprime (k ^ m) (l ^ n)
theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : ) (d : k m) :
k = 1
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
• One or more equations did not get rendered due to their size.
Instances For
theorem Nat.gcd_mul_dvd_mul_gcd (k : Nat) (m : Nat) (n : Nat) :
Nat.gcd k (m * n) Nat.gcd k m * Nat.gcd k n
theorem Nat.Coprime.gcd_mul {m : Nat} {n : Nat} (k : Nat) (h : ) :
Nat.gcd k (m * n) = Nat.gcd k m * Nat.gcd k n
theorem Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {c : Nat} {d : Nat} {a : Nat} {b : Nat} (cop : ) (h : a * b = c * d) :
Nat.gcd a c * Nat.gcd b c = c