Documentation

def Nat.xgcdAux :

ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ

Helper function for the extended GCD algorithm (Nat.xgcd).

Instances For

@[simp]

theorem Nat.xgcd_zero_left {s t : ℤ} {r' : ℕ} {s' t' : ℤ} :

xgcdAux 0 s t r' s' t' = (r', s', t')

theorem Nat.xgcdAux_rec {r : ℕ} {s t : ℤ} {r' : ℕ} {s' t' : ℤ} (h : 0 < r) :

r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

def Nat.xgcd (x y : ℕ) :

ℤ × ℤ

Use the extended GCD algorithm to generate the a and b values satisfying gcd x y = x * a + y * b.

Instances For

def Nat.gcdA (x y : ℕ) :

ℤ

The extended GCD a value in the equation gcd x y = x * a + y * b.

Instances For

def Nat.gcdB (x y : ℕ) :

ℤ

The extended GCD b value in the equation gcd x y = x * a + y * b.

Instances For

@[simp]

theorem Nat.gcdA_zero_left {s : ℕ} :

gcdA 0 s = 0

@[simp]

theorem Nat.gcdB_zero_left {s : ℕ} :

gcdB 0 s = 1

@[simp]

theorem Nat.gcdA_zero_right {s : ℕ} (h : s ≠ 0) :

s.gcdA 0 = 1

@[simp]

theorem Nat.gcdB_zero_right {s : ℕ} (h : s ≠ 0) :

s.gcdB 0 = 0

@[simp]

theorem Nat.xgcdAux_fst (x y : ℕ) (s t s' t' : ℤ) :

(x.xgcdAux s t y s' t').1 = x.gcd y

theorem Nat.xgcdAux_val (x y : ℕ) :

x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

theorem Nat.xgcd_val (x y : ℕ) :

x.xgcd y = (x.gcdA y, x.gcdB y)

theorem Nat.gcd_eq_gcd_ab (x y : ℕ) :

↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Bézout's lemma: given x y : ℕ, gcd x y = x * a + y * b, where a = gcd_a x y and b = gcd_b x y are computed by the extended Euclidean algorithm.

theorem Nat.exists_mul_mod_eq_gcd {k n : ℕ} (hk : n.gcd k < k) :

∃ m < k, n * m % k = n.gcd k

@[deprecated Nat.exists_mul_mod_eq_gcd (since := "2025-11-01")]

theorem Nat.exists_mul_emod_eq_gcd {k n : ℕ} (hk : n.gcd k < k) :

∃ m < k, n * m % k = n.gcd k

Alias of Nat.exists_mul_mod_eq_gcd.

theorem Nat.exists_mul_mod_eq_one_of_coprime {k n : ℕ} (hkn : n.Coprime k) (hk : 1 < k) :

∃ m < k, n * m % k = 1

@[deprecated Nat.exists_mul_mod_eq_one_of_coprime (since := "2025-11-01")]

theorem Nat.exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : n.Coprime k) (hk : 1 < k) :

∃ m < k, n * m % k = 1

Alias of Nat.exists_mul_mod_eq_one_of_coprime.

theorem Nat.exists_mul_mod_eq_of_coprime {k n : ℕ} (r : ℕ) (hkn : n.Coprime k) (hk : k ≠ 0) :

∃ m < k, n * m % k = r % k

Divisibility over ℤ #

theorem Int.gcd_def (i j : ℤ) :

i.gcd j = i.natAbs.gcd j.natAbs

def Int.gcdA :

ℤ → ℤ → ℤ

The extended GCD a value in the equation gcd x y = x * a + y * b.

Instances For

def Int.gcdB :

ℤ → ℤ → ℤ

The extended GCD b value in the equation gcd x y = x * a + y * b.

Instances For

theorem Int.gcd_eq_gcd_ab (x y : ℤ) :

↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y

Bézout's lemma

theorem Int.lcm_def (i j : ℤ) :

i.lcm j = i.natAbs.lcm j.natAbs

theorem Int.gcd_div {a b c : ℤ} (ha : c ∣ a) (hb : c ∣ b) :

(a / c).gcd (b / c) = a.gcd b / c.natAbs

Alias of Int.gcd_ediv.

theorem Int.gcd_div_gcd_div_gcd {i j : ℤ} (h : 0 < i.gcd j) :

(i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1

Alias of Int.gcd_ediv_gcd_ediv_gcd.

theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_left {a : ℤ} {m n : ℕ} (h : a.gcd (↑m * ↑n) = 1) :

a.gcd ↑m = 1

If gcd a (m * n) = 1, then gcd a m = 1.

theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_right {a : ℤ} {m n : ℕ} (h : a.gcd (↑m * ↑n) = 1) :

a.gcd ↑n = 1

If gcd a (m * n) = 1, then gcd a n = 1.

theorem Int.ne_zero_of_gcd {x y : ℤ} (hc : x.gcd y ≠ 0) :

x ≠ 0 ∨ y ≠ 0

theorem Int.exists_gcd_one {m n : ℤ} (H : 0 < m.gcd n) :

∃ (m' : ℤ) (n' : ℤ), m'.gcd n' = 1 ∧ m = m' * ↑(m.gcd n) ∧ n = n' * ↑(m.gcd n)

theorem Int.exists_gcd_one' {m n : ℤ} (H : 0 < m.gcd n) :

∃ (g : ℕ) (m' : ℤ) (n' : ℤ), 0 < g ∧ m'.gcd n' = 1 ∧ m = m' * ↑g ∧ n = n' * ↑g

theorem Int.gcd_dvd_iff {a b : ℤ} {n : ℕ} :

a.gcd b ∣ n ↔ ∃ (x : ℤ) (y : ℤ), ↑n = a * x + b * y

theorem Int.gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : ℤ), e ∣ a → e ∣ b → e ∣ d) :

d = ↑(a.gcd b)

theorem Int.dvd_of_dvd_mul_left_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : a.gcd c = 1) :

a ∣ b

Euclid's lemma: if a ∣ b * c and gcd a c = 1 then a ∣ b. Compare with IsCoprime.dvd_of_dvd_mul_left and UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors

theorem Int.dvd_of_dvd_mul_right_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : a.gcd b = 1) :

a ∣ c

Euclid's lemma: if a ∣ b * c and gcd a b = 1 then a ∣ c. Compare with IsCoprime.dvd_of_dvd_mul_right and UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors

theorem Int.gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :

IsLeast {n : ℕ | 0 < n ∧ ∃ (x : ℤ) (y : ℤ), ↑n = a * x + b * y} (a.gcd b)

For nonzero integers a and b, gcd a b is the smallest positive natural number that can be written in the form a * x + b * y for some pair of integers x and y