Documentation

Mathlib.Data.Nat.GCD.Basic

Properties of Nat.gcd, Nat.lcm, and Nat.Coprime #

Definitions are provided in batteries.

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

Note that the global IsCoprime is not a straightforward generalization of Nat.Coprime, see Nat.isCoprime_iff_coprime for the connection between the two.

Most of this file could be moved to batteries as well.

gcd #

source
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

Lemmas where one argument consists of addition of a multiple of the other

source
@[simp]
theorem Nat.gcd_add_mul_right_right (m n k : ℕ) :
m.gcd (n + k * m) = m.gcd n
source
@[simp]
theorem Nat.gcd_add_mul_left_right (m n k : ℕ) :
m.gcd (n + m * k) = m.gcd n
source
@[simp]
theorem Nat.gcd_mul_right_add_right (m n k : ℕ) :
m.gcd (k * m + n) = m.gcd n
source
@[simp]
theorem Nat.gcd_mul_left_add_right (m n k : ℕ) :
m.gcd (m * k + n) = m.gcd n
source
@[simp]
theorem Nat.gcd_add_mul_right_left (m n k : ℕ) :
(m + k * n).gcd n = m.gcd n
source
@[simp]
theorem Nat.gcd_add_mul_left_left (m n k : ℕ) :
(m + n * k).gcd n = m.gcd n
source
@[simp]
theorem Nat.gcd_mul_right_add_left (m n k : ℕ) :
(k * n + m).gcd n = m.gcd n
source
@[simp]
theorem Nat.gcd_mul_left_add_left (m n k : ℕ) :
(n * k + m).gcd n = m.gcd n

Lemmas where one argument consists of an addition of the other

source
@[simp]
theorem Nat.gcd_add_self_right (m n : ℕ) :
m.gcd (n + m) = m.gcd n
source
@[simp]
theorem Nat.gcd_add_self_left (m n : ℕ) :
(m + n).gcd n = m.gcd n
source
@[simp]
theorem Nat.gcd_self_add_left (m n : ℕ) :
(m + n).gcd m = n.gcd m
source
@[simp]
theorem Nat.gcd_self_add_right (m n : ℕ) :
m.gcd (m + n) = m.gcd n

Lemmas where one argument consists of a subtraction of the other

source
@[simp]
theorem Nat.gcd_sub_self_left {m n : ℕ} (h : m ≤ n) :
(n - m).gcd m = n.gcd m
source
@[simp]
theorem Nat.gcd_sub_self_right {m n : ℕ} (h : m ≤ n) :
m.gcd (n - m) = m.gcd n
source
@[simp]
theorem Nat.gcd_self_sub_left {m n : ℕ} (h : m ≤ n) :
(n - m).gcd n = m.gcd n
source
@[simp]
theorem Nat.gcd_self_sub_right {m n : ℕ} (h : m ≤ n) :
n.gcd (n - m) = n.gcd m
source
@[simp, irreducible]
theorem Nat.pow_sub_one_mod_pow_sub_one (a b c : ℕ) :
(a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
source
@[simp, irreducible]
theorem Nat.pow_sub_one_gcd_pow_sub_one (a b c : ℕ) :
(a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

lcm #

source
theorem Nat.lcm_dvd_mul (m n : ℕ) :
m.lcm n ∣ m * n
source
theorem Nat.lcm_dvd_iff {m n k : ℕ} :
m.lcm n ∣ k ↔ m ∣ k ∧ n ∣ k
source
theorem Nat.lcm_pos {m n : ℕ} :
0 < m → 0 < n → 0 < m.lcm n
source
theorem Nat.lcm_mul_left {m n k : ℕ} :
(m * n).lcm (m * k) = m * n.lcm k
source
theorem Nat.lcm_mul_right {m n k : ℕ} :
(m * n).lcm (k * n) = m.lcm k * n

Coprime #

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

source
theorem Nat.Coprime.lcm_eq_mul {m n : ℕ} (h : m.Coprime n) :
m.lcm n = m * n
source
theorem Nat.Coprime.symmetric :
Symmetric Coprime
source
theorem Nat.Coprime.dvd_mul_right {m n k : ℕ} (H : k.Coprime n) :
k ∣ m * n ↔ k ∣ m
source
theorem Nat.Coprime.dvd_mul_left {m n k : ℕ} (H : k.Coprime m) :
k ∣ m * n ↔ k ∣ n
source
@[simp]
theorem Nat.coprime_add_self_right {m n : ℕ} :
m.Coprime (n + m) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_self_add_right {m n : ℕ} :
m.Coprime (m + n) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_add_self_left {m n : ℕ} :
(m + n).Coprime n ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_self_add_left {m n : ℕ} :
(m + n).Coprime m ↔ n.Coprime m
source
@[simp]
theorem Nat.coprime_add_mul_right_right (m n k : ℕ) :
m.Coprime (n + k * m) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_add_mul_left_right (m n k : ℕ) :
m.Coprime (n + m * k) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_mul_right_add_right (m n k : ℕ) :
m.Coprime (k * m + n) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_mul_left_add_right (m n k : ℕ) :
m.Coprime (m * k + n) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_add_mul_right_left (m n k : ℕ) :
(m + k * n).Coprime n ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_add_mul_left_left (m n k : ℕ) :
(m + n * k).Coprime n ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_mul_right_add_left (m n k : ℕ) :
(k * n + m).Coprime n ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_mul_left_add_left (m n k : ℕ) :
(n * k + m).Coprime n ↔ m.Coprime n
source
theorem Nat.add_coprime_iff_left {a b c : ℕ} (h : c ∣ b) :
(a + b).Coprime c ↔ a.Coprime c
source
theorem Nat.add_coprime_iff_right {a b c : ℕ} (h : c ∣ a) :
(a + b).Coprime c ↔ b.Coprime c
source
theorem Nat.coprime_add_iff_left {a b c : ℕ} (h : a ∣ c) :
a.Coprime (b + c) ↔ a.Coprime b
source
theorem Nat.coprime_add_iff_right {a b c : ℕ} (h : a ∣ b) :
a.Coprime (b + c) ↔ a.Coprime c
source
theorem Nat.Coprime.of_dvd_left {a₁ a₂ b : ℕ} (ha : a₁ ∣ a₂) (h : a₂.Coprime b) :
a₁.Coprime b
source
theorem Nat.Coprime.of_dvd_right {a b₁ b₂ : ℕ} (hb : b₁ ∣ b₂) (h : a.Coprime b₂) :
a.Coprime b₁
source
theorem Nat.Coprime.of_dvd {a₁ a₂ b₁ b₂ : ℕ} (ha : a₁ ∣ a₂) (hb : b₁ ∣ b₂) (h : a₂.Coprime b₂) :
a₁.Coprime b₁
source
@[simp]
theorem Nat.coprime_sub_self_left {m n : ℕ} (h : m ≤ n) :
(n - m).Coprime m ↔ n.Coprime m
source
@[simp]
theorem Nat.coprime_sub_self_right {m n : ℕ} (h : m ≤ n) :
m.Coprime (n - m) ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_self_sub_left {m n : ℕ} (h : m ≤ n) :
(n - m).Coprime n ↔ m.Coprime n
source
@[simp]
theorem Nat.coprime_self_sub_right {m n : ℕ} (h : m ≤ n) :
n.Coprime (n - m) ↔ n.Coprime m
source
@[simp]
theorem Nat.coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
(a ^ n).Coprime b ↔ a.Coprime b
source
@[simp]
theorem Nat.coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
a.Coprime (b ^ n) ↔ a.Coprime b
source
theorem Nat.not_coprime_zero_zero :
¬Coprime 0 0
source
theorem Nat.coprime_one_left_iff (n : ℕ) :
Coprime 1 n ↔ True
source
theorem Nat.coprime_one_right_iff (n : ℕ) :
n.Coprime 1 ↔ True
source
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
source
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
source
def Nat.prodDvdAndDvdOfDvdProd {m n k : ℕ} (H : k ∣ m * n) :
{ d : { m' : ℕ // m' ∣ m } × { n' : ℕ // n' ∣ n } // k = ↑d.1 * ↑d.2 }

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 GCDMonoids.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Nat.dvd_mul {x m n : ℕ} :
    x ∣ m * n ↔ ∃ (y : ℕ), ∃ (z : ℕ), y ∣ m ∧ z ∣ n ∧ y * z = x
    source
    theorem Nat.pow_dvd_pow_iff {a b n : ℕ} (n0 : n ≠ 0) :
    a ^ n ∣ b ^ n ↔ a ∣ b
    source
    theorem Nat.coprime_iff_isRelPrime {m n : ℕ} :
    m.Coprime n ↔ IsRelPrime m n
    source
    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

    source
    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
    source
    theorem Nat.dvd_gcd_mul_iff_dvd_mul {x n m : ℕ} :
    x ∣ x.gcd n * m ↔ x ∣ n * m
    source
    theorem Nat.dvd_mul_gcd_iff_dvd_mul {x n m : ℕ} :
    x ∣ n * x.gcd m ↔ x ∣ n * m
    source
    theorem Nat.dvd_gcd_mul_gcd_iff_dvd_mul {x n m : ℕ} :
    x ∣ x.gcd n * x.gcd m ↔ x ∣ n * m
    source
    theorem Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime {x n m : ℕ} (hcop : n.Coprime m) :
    x.gcd n * x.gcd m = x ↔ x ∣ n * m