mathlib3 documentation

data.nat.gcd.basic

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Generalizations of these are provided in a later file as gcd_monoid.gcd and gcd_monoid.lcm.

Note that the global is_coprime is not a straightforward generalization of nat.coprime, see nat.is_coprime_iff_coprime for the connection between the two.

gcd #

theorem nat.gcd_dvd (m n : ) :
m.gcd n m m.gcd n n
theorem nat.gcd_dvd_left (m n : ) :
m.gcd n m
theorem nat.gcd_dvd_right (m n : ) :
m.gcd n n
theorem nat.gcd_le_left {m : } (n : ) (h : 0 < m) :
m.gcd n m
theorem nat.gcd_le_right (m : ) {n : } (h : 0 < n) :
m.gcd n n
theorem nat.dvd_gcd {m n k : } :
k m k n k m.gcd n
theorem nat.dvd_gcd_iff {m n k : } :
k m.gcd n k m k n
theorem nat.gcd_comm (m n : ) :
m.gcd n = n.gcd m
theorem nat.gcd_eq_left_iff_dvd {m n : } :
m n m.gcd n = m
theorem nat.gcd_eq_right_iff_dvd {m n : } :
m n n.gcd m = m
theorem nat.gcd_assoc (m n k : ) :
(m.gcd n).gcd k = m.gcd (n.gcd k)
@[simp]
theorem nat.gcd_one_right (n : ) :
n.gcd 1 = 1
theorem nat.gcd_mul_left (m n k : ) :
(m * n).gcd (m * k) = m * n.gcd k
theorem nat.gcd_mul_right (m n k : ) :
(m * n).gcd (k * n) = m.gcd k * n
theorem nat.gcd_pos_of_pos_left {m : } (n : ) (mpos : 0 < m) :
0 < m.gcd n
theorem nat.gcd_pos_of_pos_right (m : ) {n : } (npos : 0 < n) :
0 < m.gcd n
theorem nat.eq_zero_of_gcd_eq_zero_left {m n : } (H : m.gcd n = 0) :
m = 0
theorem nat.eq_zero_of_gcd_eq_zero_right {m n : } (H : m.gcd n = 0) :
n = 0
@[simp]
theorem nat.gcd_eq_zero_iff {i j : } :
i.gcd j = 0 i = 0 j = 0
theorem nat.gcd_div {m n k : } (H1 : k m) (H2 : k n) :
(m / k).gcd (n / k) = m.gcd n / k
theorem nat.gcd_greatest {a b d : } (hda : d a) (hdb : d b) (hd : (e : ), e a e b e d) :
d = a.gcd b
theorem nat.gcd_dvd_gcd_of_dvd_left {m k : } (n : ) (H : m k) :
m.gcd n k.gcd n
theorem nat.gcd_dvd_gcd_of_dvd_right {m k : } (n : ) (H : m k) :
n.gcd m n.gcd k
theorem nat.gcd_dvd_gcd_mul_left (m n k : ) :
m.gcd n (k * m).gcd n
theorem nat.gcd_dvd_gcd_mul_right (m n k : ) :
m.gcd n (m * k).gcd n
theorem nat.gcd_dvd_gcd_mul_left_right (m n k : ) :
m.gcd n m.gcd (k * n)
theorem nat.gcd_dvd_gcd_mul_right_right (m n k : ) :
m.gcd n m.gcd (n * k)
theorem nat.gcd_eq_left {m n : } (H : m n) :
m.gcd n = m
theorem nat.gcd_eq_right {m n : } (H : n m) :
m.gcd n = n
@[simp]
theorem nat.gcd_mul_left_left (m n : ) :
(m * n).gcd n = n
@[simp]
theorem nat.gcd_mul_left_right (m n : ) :
n.gcd (m * n) = n
@[simp]
theorem nat.gcd_mul_right_left (m n : ) :
(n * m).gcd n = n
@[simp]
theorem nat.gcd_mul_right_right (m n : ) :
n.gcd (n * m) = n
@[simp]
theorem nat.gcd_gcd_self_right_left (m n : ) :
m.gcd (m.gcd n) = m.gcd n
@[simp]
theorem nat.gcd_gcd_self_right_right (m n : ) :
m.gcd (n.gcd m) = n.gcd m
@[simp]
theorem nat.gcd_gcd_self_left_right (m n : ) :
(n.gcd m).gcd m = n.gcd m
@[simp]
theorem nat.gcd_gcd_self_left_left (m n : ) :
(m.gcd n).gcd m = m.gcd n
@[simp]
theorem nat.gcd_add_mul_right_right (m n k : ) :
m.gcd (n + k * m) = m.gcd n
@[simp]
theorem nat.gcd_add_mul_left_right (m n k : ) :
m.gcd (n + m * k) = m.gcd n
@[simp]
theorem nat.gcd_mul_right_add_right (m n k : ) :
m.gcd (k * m + n) = m.gcd n
@[simp]
theorem nat.gcd_mul_left_add_right (m n k : ) :
m.gcd (m * k + n) = m.gcd n
@[simp]
theorem nat.gcd_add_mul_right_left (m n k : ) :
(m + k * n).gcd n = m.gcd n
@[simp]
theorem nat.gcd_add_mul_left_left (m n k : ) :
(m + n * k).gcd n = m.gcd n
@[simp]
theorem nat.gcd_mul_right_add_left (m n k : ) :
(k * n + m).gcd n = m.gcd n
@[simp]
theorem nat.gcd_mul_left_add_left (m n k : ) :
(n * k + m).gcd n = m.gcd n
@[simp]
theorem nat.gcd_add_self_right (m n : ) :
m.gcd (n + m) = m.gcd n
@[simp]
theorem nat.gcd_add_self_left (m n : ) :
(m + n).gcd n = m.gcd n
@[simp]
theorem nat.gcd_self_add_left (m n : ) :
(m + n).gcd m = n.gcd m
@[simp]
theorem nat.gcd_self_add_right (m n : ) :
m.gcd (m + n) = m.gcd n

lcm #

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

coprime #

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

@[protected, instance]
Equations
theorem nat.coprime_iff_gcd_eq_one {m n : } :
m.coprime n m.gcd n = 1
theorem nat.coprime.gcd_eq_one {m n : } (h : m.coprime n) :
m.gcd n = 1
theorem nat.coprime.lcm_eq_mul {m n : } (h : m.coprime n) :
m.lcm n = m * n
theorem nat.coprime.symm {m n : } :
theorem nat.coprime_comm {m n : } :
theorem nat.coprime.dvd_of_dvd_mul_right {m n k : } (H1 : k.coprime n) (H2 : k m * n) :
k m
theorem nat.coprime.dvd_of_dvd_mul_left {m n k : } (H1 : k.coprime m) (H2 : k m * n) :
k n
theorem nat.coprime.dvd_mul_right {m n k : } (H : k.coprime n) :
k m * n k m
theorem nat.coprime.dvd_mul_left {m n k : } (H : k.coprime m) :
k m * n k n
theorem nat.coprime.gcd_mul_left_cancel {k : } (m : ) {n : } (H : k.coprime n) :
(k * m).gcd n = m.gcd n
theorem nat.coprime.gcd_mul_right_cancel (m : ) {k n : } (H : k.coprime n) :
(m * k).gcd n = m.gcd n
theorem nat.coprime.gcd_mul_left_cancel_right {k m : } (n : ) (H : k.coprime m) :
m.gcd (k * n) = m.gcd n
theorem nat.coprime.gcd_mul_right_cancel_right {k m : } (n : ) (H : k.coprime m) :
m.gcd (n * k) = m.gcd n
theorem nat.coprime_div_gcd_div_gcd {m n : } (H : 0 < m.gcd n) :
(m / m.gcd n).coprime (n / m.gcd n)
theorem nat.not_coprime_of_dvd_of_dvd {m n d : } (dgt1 : 1 < d) (Hm : d m) (Hn : d n) :
theorem nat.exists_coprime {m n : } (H : 0 < m.gcd n) :
(m' n' : ), m'.coprime n' m = m' * m.gcd n n = n' * m.gcd n
theorem nat.exists_coprime' {m n : } (H : 0 < m.gcd n) :
(g m' n' : ), 0 < g m'.coprime n' m = m' * g n = n' * g
@[simp]
theorem nat.coprime_add_self_right {m n : } :
m.coprime (n + m) m.coprime n
@[simp]
theorem nat.coprime_self_add_right {m n : } :
m.coprime (m + n) m.coprime n
@[simp]
theorem nat.coprime_add_self_left {m n : } :
(m + n).coprime n m.coprime n
@[simp]
theorem nat.coprime_self_add_left {m n : } :
(m + n).coprime m n.coprime m
@[simp]
theorem nat.coprime_add_mul_right_right (m n k : ) :
m.coprime (n + k * m) m.coprime n
@[simp]
theorem nat.coprime_add_mul_left_right (m n k : ) :
m.coprime (n + m * k) m.coprime n
@[simp]
theorem nat.coprime_mul_right_add_right (m n k : ) :
m.coprime (k * m + n) m.coprime n
@[simp]
theorem nat.coprime_mul_left_add_right (m n k : ) :
m.coprime (m * k + n) m.coprime n
@[simp]
theorem nat.coprime_add_mul_right_left (m n k : ) :
(m + k * n).coprime n m.coprime n
@[simp]
theorem nat.coprime_add_mul_left_left (m n k : ) :
(m + n * k).coprime n m.coprime n
@[simp]
theorem nat.coprime_mul_right_add_left (m n k : ) :
(k * n + m).coprime n m.coprime n
@[simp]
theorem nat.coprime_mul_left_add_left (m n k : ) :
(n * k + m).coprime n m.coprime n
theorem nat.coprime.mul {m n k : } (H1 : m.coprime k) (H2 : n.coprime k) :
(m * n).coprime k
theorem nat.coprime.mul_right {k m n : } (H1 : k.coprime m) (H2 : k.coprime n) :
k.coprime (m * n)
theorem nat.coprime.coprime_dvd_left {m k n : } (H1 : m k) (H2 : k.coprime n) :
theorem nat.coprime.coprime_dvd_right {m k n : } (H1 : n m) (H2 : k.coprime m) :
theorem nat.coprime.coprime_mul_left {k m n : } (H : (k * m).coprime n) :
theorem nat.coprime.coprime_mul_right {k m n : } (H : (m * k).coprime n) :
theorem nat.coprime.coprime_mul_left_right {k m n : } (H : m.coprime (k * n)) :
theorem nat.coprime.coprime_mul_right_right {k m n : } (H : m.coprime (n * k)) :
theorem nat.coprime.coprime_div_left {m n a : } (cmn : m.coprime n) (dvd : a m) :
(m / a).coprime n
theorem nat.coprime.coprime_div_right {m n a : } (cmn : m.coprime n) (dvd : a n) :
m.coprime (n / a)
theorem nat.coprime_mul_iff_left {k m n : } :
(m * n).coprime k m.coprime k n.coprime k
theorem nat.coprime_mul_iff_right {k m n : } :
k.coprime (m * n) k.coprime m k.coprime n
theorem nat.coprime.gcd_left (k : ) {m n : } (hmn : m.coprime n) :
(k.gcd m).coprime n
theorem nat.coprime.gcd_right (k : ) {m n : } (hmn : m.coprime n) :
m.coprime (k.gcd n)
theorem nat.coprime.gcd_both (k l : ) {m n : } (hmn : m.coprime n) :
(k.gcd m).coprime (l.gcd n)
theorem nat.coprime.mul_dvd_of_dvd_of_dvd {a n m : } (hmn : m.coprime n) (hm : m a) (hn : n a) :
m * n a
theorem nat.coprime_one_left (n : ) :
theorem nat.coprime_one_right (n : ) :
theorem nat.coprime.pow_left {m k : } (n : ) (H1 : m.coprime k) :
(m ^ n).coprime k
theorem nat.coprime.pow_right {m k : } (n : ) (H1 : k.coprime m) :
k.coprime (m ^ n)
theorem nat.coprime.pow {k l : } (m n : ) (H1 : k.coprime l) :
(k ^ m).coprime (l ^ n)
@[simp]
theorem nat.coprime_pow_left_iff {n : } (hn : 0 < n) (a b : ) :
(a ^ n).coprime b a.coprime b
@[simp]
theorem nat.coprime_pow_right_iff {n : } (hn : 0 < n) (a b : ) :
a.coprime (b ^ n) a.coprime b
theorem nat.coprime.eq_one_of_dvd {k m : } (H : k.coprime m) (d : k m) :
k = 1
@[simp]
theorem nat.coprime_zero_left (n : ) :
0.coprime n n = 1
@[simp]
theorem nat.coprime_zero_right (n : ) :
n.coprime 0 n = 1
@[simp]
@[simp]
@[simp]
theorem nat.coprime_self (n : ) :
n.coprime n n = 1
theorem nat.gcd_mul_of_coprime_of_dvd {a b c : } (hac : a.coprime c) (b_dvd_c : b c) :
(a * b).gcd c = b
theorem nat.coprime.eq_of_mul_eq_zero {m n : } (h : m.coprime n) (hmn : m * n = 0) :
m = 0 n = 1 m = 1 n = 0
def nat.prod_dvd_and_dvd_of_dvd_prod {m n k : } (H : k m * n) :
{d // k = (d.fst) * (d.snd)}

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

See exists_dvd_and_dvd_of_dvd_mul for the more general but less constructive version for other gcd_monoids.

Equations
theorem nat.dvd_mul {x m n : } :
x m * n (y z : ), y m z n y * z = x
theorem nat.gcd_mul_dvd_mul_gcd (k m n : ) :
k.gcd (m * n) k.gcd m * k.gcd n
theorem nat.coprime.gcd_mul (k : ) {m n : } (h : m.coprime n) :
k.gcd (m * n) = k.gcd m * k.gcd n
theorem nat.pow_dvd_pow_iff {a b n : } (n0 : 0 < n) :
a ^ n b ^ n a b
theorem nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {a b c d : } (cop : c.coprime d) (h : a * b = c * d) :
a.gcd c * b.gcd c = c
theorem nat.eq_one_of_dvd_coprimes {a b k : } (h_ab_coprime : a.coprime b) (hka : k a) (hkb : k b) :
k = 1

If k:ℕ divides coprime a and b then k = 1

theorem nat.coprime.mul_add_mul_ne_mul {m n a b : } (cop : m.coprime n) (ha : a 0) (hb : b 0) :
a * m + b * n m * n