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]

def nat.coprime.decidable (m n : ℕ) :

decidable (m.coprime n)

Equations

nat.coprime.decidable m n = _.mpr (nat.decidable_eq (m.gcd n) 1)

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 : ℕ} :

n.coprime m → m.coprime n

theorem nat.coprime_comm {m n : ℕ} :

n.coprime m ↔ m.coprime n

theorem nat.coprime.symmetric :

symmetric nat.coprime

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

theorem nat.not_coprime_zero_zero :

@[simp]

theorem nat.coprime_one_left_iff (n : ℕ) :

1.coprime n ↔ true

@[simp]

theorem nat.coprime_one_right_iff (n : ℕ) :

n.coprime 1 ↔ true

@[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

nat.prod_dvd_and_dvd_of_dvd_prod H = (λ (_x : ℕ) (h0 : k.gcd m = _x), _x.cases_on (λ (h0 : k.gcd m = 0), eq.rec (λ (H : 0 ∣ m * n) (h0 : 0.gcd m = 0), eq.rec (λ (H : 0 ∣ 0 * n) (h0 : 0.gcd 0 = 0), ⟨(⟨0, nat.prod_dvd_and_dvd_of_dvd_prod._proof_1⟩, ⟨n, _⟩), _⟩) _ H h0) _ H h0) (λ (n_1 : ℕ) (h0 : k.gcd m = n_1.succ), (λ (h0 : k.gcd m = n_1.succ), ⟨(⟨k.gcd m, _⟩, ⟨k / k.gcd m, _⟩), _⟩) h0) h0) (k.gcd m) nat.prod_dvd_and_dvd_of_dvd_prod._proof_7

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