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
source
theorem Nat.gcd_right_comm (a b c : ℕ) :
(a.gcd b).gcd c = (a.gcd c).gcd b

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

source
@[simp]
theorem Nat.pow_sub_one_mod_pow_sub_one (a b c : ℕ) :
(a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
source
@[simp]
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 and divisibility #

source
theorem Nat.dvd_lcm_of_dvd_left {a b : ℕ} (h : a ∣ b) (c : ℕ) :
a ∣ b.lcm c
source
theorem Nat.Dvd.dvd.nat_lcm_right {a b : ℕ} (h : a ∣ b) (c : ℕ) :
a ∣ b.lcm c

Alias of Nat.dvd_lcm_of_dvd_left.

source
theorem Nat.dvd_of_lcm_right_dvd {a b c : ℕ} (h : a.lcm b ∣ c) :
a ∣ c
source
theorem Nat.dvd_lcm_of_dvd_right {a b : ℕ} (h : a ∣ b) (c : ℕ) :
a ∣ c.lcm b
source
theorem Nat.Dvd.dvd.nat_lcm_left {a b : ℕ} (h : a ∣ b) (c : ℕ) :
a ∣ c.lcm b

Alias of Nat.dvd_lcm_of_dvd_right.

source
theorem Nat.dvd_of_lcm_left_dvd {a b c : ℕ} (h : a.lcm b ∣ c) :
b ∣ c

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
instance Nat.Coprime.stdSymm :
Std.Symm Coprime
source
@[deprecated Nat.Coprime.stdSymm (since := "2026-06-10")]
theorem Nat.Coprime.symmetric :
Std.Symm Coprime

Alias of Nat.Coprime.stdSymm.

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
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.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
source
theorem Nat.div_mul_div {n m k : ℕ} (hkm : m ∣ k) (hkn : n ∣ m) :
k / m * (m / n) = k / n
source
theorem Nat.div_dvd_div_left {n m k : ℕ} (hkm : m ∣ k) (hkn : n ∣ m) :
k / m ∣ k / n
source
theorem Nat.div_lcm_eq_div_gcd {n m k : ℕ} (hkm : m ∣ k) (hkn : n ∣ k) :
(k / m).lcm (k / n) = k / m.gcd n