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 : ) :
0 < mm.gcd n m

theorem nat.gcd_le_right (m : ) {n : } :
0 < nm.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 : ) :
0 < m0 < m.gcd n

theorem nat.gcd_pos_of_pos_right (m : ) {n : } :
0 < n0 < m.gcd n

theorem nat.eq_zero_of_gcd_eq_zero_left {m n : } :
m.gcd n = 0m = 0

theorem nat.eq_zero_of_gcd_eq_zero_right {m n : } :
m.gcd n = 0n = 0

theorem nat.gcd_div {m n k : } :
k mk n(m / k).gcd (n / k) = m.gcd n / k

theorem nat.gcd_dvd_gcd_of_dvd_left {m k : } (n : ) :
m km.gcd n k.gcd n

theorem nat.gcd_dvd_gcd_of_dvd_right {m k : } (n : ) :
m kn.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 : } :
m nm.gcd n = m

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

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 : } :
m kn km.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]
def nat.decidable (m n : ) :

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 : } :
k.coprime nk m * nk m

theorem nat.coprime.dvd_of_dvd_mul_left {m n k : } :
k.coprime mk m * nk n

theorem nat.coprime.gcd_mul_left_cancel {k : } (m : ) {n : } :
k.coprime n(k * m).gcd n = m.gcd n

theorem nat.coprime.gcd_mul_right_cancel (m : ) {k n : } :
k.coprime n(m * k).gcd n = m.gcd n

theorem nat.coprime.gcd_mul_left_cancel_right {k m : } (n : ) :
k.coprime mm.gcd (k * n) = m.gcd n

theorem nat.coprime.gcd_mul_right_cancel_right {k m : } (n : ) :
k.coprime mm.gcd (n * k) = m.gcd n

theorem nat.coprime_div_gcd_div_gcd {m n : } :
0 < m.gcd n(m / m.gcd n).coprime (n / m.gcd n)

theorem nat.not_coprime_of_dvd_of_dvd {m n d : } :
1 < dd md n¬m.coprime n

theorem nat.exists_coprime {m n : } :
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 : } :
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 : } :
m.coprime kn.coprime k(m * n).coprime k

theorem nat.coprime.mul_right {k m n : } :
k.coprime mk.coprime nk.coprime (m * n)

theorem nat.coprime.coprime_dvd_left {m k n : } :
m kk.coprime nm.coprime n

theorem nat.coprime.coprime_dvd_right {m k n : } :
n mk.coprime mk.coprime n

theorem nat.coprime.coprime_mul_left {k m n : } :
(k * m).coprime nm.coprime n

theorem nat.coprime.coprime_mul_right {k m n : } :
(m * k).coprime nm.coprime n

theorem nat.coprime.coprime_mul_left_right {k m n : } :
m.coprime (k * n)m.coprime n

theorem nat.coprime.coprime_mul_right_right {k m n : } :
m.coprime (n * k)m.coprime n

theorem nat.coprime.coprime_div_left {m n a : } :
m.coprime na m(m / a).coprime n

theorem nat.coprime.coprime_div_right {m n a : } :
m.coprime na nm.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 : } :
m.coprime n(k.gcd m).coprime n

theorem nat.coprime.gcd_right (k : ) {m n : } :
m.coprime nm.coprime (k.gcd n)

theorem nat.coprime.gcd_both (k l : ) {m n : } :
m.coprime n(k.gcd m).coprime (l.gcd n)

theorem nat.coprime.mul_dvd_of_dvd_of_dvd {a n m : } :
m.coprime nm an am * n a

theorem nat.coprime_one_left (n : ) :

theorem nat.coprime_one_right (n : ) :

theorem nat.coprime.pow_left {m k : } (n : ) :
m.coprime k(m ^ n).coprime k

theorem nat.coprime.pow_right {m k : } (n : ) :
k.coprime mk.coprime (m ^ n)

theorem nat.coprime.pow {k l : } (m n : ) :
k.coprime l(k ^ m).coprime (l ^ n)

theorem nat.coprime.eq_one_of_dvd {k m : } :
k.coprime mk mk = 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 : } :
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 : } :
m.coprime nk.gcd (m * n) = (k.gcd m) * k.gcd n

theorem nat.pow_dvd_pow_iff {a b n : } :
0 < n(a ^ n b ^ n a b)

theorem nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {a b c d : } :
c.coprime da * b = c * d(a.gcd c) * b.gcd c = c