Documentation

Mathlib.Data.Nat.GCD.Basic

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

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.

gcd #

source
theorem Nat.gcd_greatest {a : ℕ} {b : ℕ} {d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d) :
d = Nat.gcd a 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 : ℕ) :
Nat.gcd m (n + k * m) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_add_mul_left_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd m (n + m * k) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_mul_right_add_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd m (k * m + n) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_mul_left_add_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd m (m * k + n) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_add_mul_right_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd (m + k * n) n = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_add_mul_left_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd (m + n * k) n = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_mul_right_add_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd (k * n + m) n = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_mul_left_add_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.gcd (n * k + m) n = Nat.gcd m n

Lemmas where one argument consists of an addition of the other

source
@[simp]
theorem Nat.gcd_add_self_right (m : ℕ) (n : ℕ) :
Nat.gcd m (n + m) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_add_self_left (m : ℕ) (n : ℕ) :
Nat.gcd (m + n) n = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_self_add_left (m : ℕ) (n : ℕ) :
Nat.gcd (m + n) m = Nat.gcd n m
source
@[simp]
theorem Nat.gcd_self_add_right (m : ℕ) (n : ℕ) :
Nat.gcd m (m + n) = Nat.gcd m 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) :
Nat.gcd (n - m) m = Nat.gcd n m
source
@[simp]
theorem Nat.gcd_sub_self_right {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.gcd m (n - m) = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_self_sub_left {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.gcd (n - m) n = Nat.gcd m n
source
@[simp]
theorem Nat.gcd_self_sub_right {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.gcd n (n - m) = Nat.gcd n m

lcm #

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

Coprime #

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

source
instance Nat.instDecidableCoprime_1 (m : ℕ) (n : ℕ) :
Decidable (Nat.Coprime m n)
Equations
source
theorem Nat.Coprime.lcm_eq_mul {m : ℕ} {n : ℕ} (h : Nat.Coprime m n) :
Nat.lcm m n = m * n
source
theorem Nat.Coprime.symmetric :
Symmetric Nat.Coprime
source
theorem Nat.Coprime.dvd_mul_right {m : ℕ} {n : ℕ} {k : ℕ} (H : Nat.Coprime k n) :
k ∣ m * n ↔ k ∣ m
source
theorem Nat.Coprime.dvd_mul_left {m : ℕ} {n : ℕ} {k : ℕ} (H : Nat.Coprime k m) :
k ∣ m * n ↔ k ∣ n
source
@[simp]
theorem Nat.coprime_add_self_right {m : ℕ} {n : ℕ} :
Nat.Coprime m (n + m) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_self_add_right {m : ℕ} {n : ℕ} :
Nat.Coprime m (m + n) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_add_self_left {m : ℕ} {n : ℕ} :
Nat.Coprime (m + n) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_self_add_left {m : ℕ} {n : ℕ} :
Nat.Coprime (m + n) m ↔ Nat.Coprime n m
source
@[simp]
theorem Nat.coprime_add_mul_right_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime m (n + k * m) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_add_mul_left_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime m (n + m * k) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_mul_right_add_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime m (k * m + n) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_mul_left_add_right (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime m (m * k + n) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_add_mul_right_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime (m + k * n) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_add_mul_left_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime (m + n * k) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_mul_right_add_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime (k * n + m) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_mul_left_add_left (m : ℕ) (n : ℕ) (k : ℕ) :
Nat.Coprime (n * k + m) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_sub_self_left {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.Coprime (n - m) m ↔ Nat.Coprime n m
source
@[simp]
theorem Nat.coprime_sub_self_right {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.Coprime m (n - m) ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_self_sub_left {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.Coprime (n - m) n ↔ Nat.Coprime m n
source
@[simp]
theorem Nat.coprime_self_sub_right {m : ℕ} {n : ℕ} (h : m ≤ n) :
Nat.Coprime n (n - m) ↔ Nat.Coprime n m
source
@[simp]
theorem Nat.coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a : ℕ) (b : ℕ) :
Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b
source
@[simp]
theorem Nat.coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a : ℕ) (b : ℕ) :
Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b
source
theorem Nat.not_coprime_zero_zero :
¬Nat.Coprime 0 0
source
theorem Nat.coprime_one_left_iff (n : ℕ) :
Nat.Coprime 1 n ↔ True
source
theorem Nat.coprime_one_right_iff (n : ℕ) :
Nat.Coprime n 1 ↔ True
source
theorem Nat.gcd_mul_of_coprime_of_dvd {a : ℕ} {b : ℕ} {c : ℕ} (hac : Nat.Coprime a c) (b_dvd_c : b ∣ c) :
Nat.gcd (a * b) c = b
source
theorem Nat.Coprime.eq_of_mul_eq_zero {m : ℕ} {n : ℕ} (h : Nat.Coprime m 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 : 0 < n) :
    a ^ n ∣ b ^ n ↔ a ∣ b
    source
    theorem Nat.coprime_iff_isRelPrime {m : ℕ} {n : ℕ} :
    Nat.Coprime m n ↔ IsRelPrime m n
    source
    theorem Nat.eq_one_of_dvd_coprimes {a : ℕ} {b : ℕ} {k : ℕ} (h_ab_coprime : Nat.Coprime a 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 : Nat.Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
    a * m + b * n ≠ m * n