mathlib documentation

data.nat.gcd

Definitions and properties of gcd, lcm, and coprime

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 mk nk 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

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_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

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

lcm

theorem nat.lcm_comm (m n : ) :
m.lcm n = n.lcm m

theorem nat.lcm_zero_left (m : ) :
0.lcm m = 0

theorem nat.lcm_zero_right (m : ) :
m.lcm 0 = 0

theorem nat.lcm_one_left (m : ) :
1.lcm m = m

theorem nat.lcm_one_right (m : ) :
m.lcm 1 = m

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_assoc (m n k : ) :
(m.lcm n).lcm k = m.lcm (n.lcm k)

coprime

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

@[instance]

Equations
theorem nat.coprime.gcd_eq_one {m n : } :
m.coprime nm.gcd n = 1

theorem nat.coprime.symm {m n : } :
n.coprime mm.coprime 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.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

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)

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

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.

Equations
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