Extended GCD and divisibility over ℤ

Main definitions

• Given x y : ℕ, xgcd x y computes the pair of integers (a, b) such that gcd x y = x * a + y * b. gcdA x y and gcdB x y are defined to be a and b, respectively.

Main statements

• gcd_eq_gcd_ab: Bézout's lemma, given x y : ℕ, gcd x y = x * gcdA x y + y * gcdB x y.

Tags

Bézout's lemma, Bezout's lemma

Extended Euclidean algorithm

def Nat.xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ

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

Equations

• Nat.xgcdAux 0 x✝³ x✝² x✝¹ x✝ x = (x✝¹, x✝, x)
• k.succ.xgcdAux x✝³ x✝² x✝¹ x✝ x = (x✝¹ % k.succ).xgcdAux (x✝ - ↑(x✝¹ / k.succ) * x✝³) (x - ↑(x✝¹ / k.succ) * x✝²) k.succ x✝³ x✝²

theorem Nat.xgcdAux_zero {s : ℤ} {t : ℤ} {r' : ℕ} {s' : ℤ} {t' : ℤ} : Nat.xgcdAux 0 s t r' s' t' = (r', s', t')

theorem Nat.xgcdAux_succ {k : ℕ} {s : ℤ} {t : ℤ} {r' : ℕ} {s' : ℤ} {t' : ℤ} : k.succ.xgcdAux s t r' s' t' = (r' % k.succ).xgcdAux (s' - ↑r' / ↑k.succ * s) (t' - ↑r' / ↑k.succ * t) k.succ s t

@[simp]

theorem Nat.xgcd_zero_left {s : ℤ} {t : ℤ} {r' : ℕ} {s' : ℤ} {t' : ℤ} : Nat.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.

Equations

• x.xgcd y = (x.xgcdAux 1 0 y 0 1).2

def Nat.gcdA (x : ℕ) (y : ℕ) : ℤ

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

Equations

• x.gcdA y = (x.xgcd y).1

def Nat.gcdB (x : ℕ) (y : ℕ) : ℤ

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

Equations

• x.gcdB y = (x.xgcd y).2

@[simp]

theorem Nat.gcdA_zero_left {s : ℕ} : Nat.gcdA 0 s = 0

@[simp]

theorem Nat.gcdB_zero_left {s : ℕ} : Nat.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.xgcdAux_P (x : ℕ) (y : ℕ) {r : ℕ} {r' : ℕ} {s : ℤ} {t : ℤ} {s' : ℤ} {t' : ℤ} : Nat.P x y (r, s, t) → Nat.P x y (r', s', t') → Nat.P x y (r.xgcdAux s t r' s' t')

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_emod_eq_gcd {k : ℕ} {n : ℕ} (hk : n.gcd k < k) : ∃ (m : ℕ), n * m % k = n.gcd k

theorem Nat.exists_mul_emod_eq_one_of_coprime {k : ℕ} {n : ℕ} (hkn : n.Coprime k) (hk : 1 < k) : ∃ (m : ℕ), n * m % k = 1

Divisibility over ℤ

theorem Int.gcd_def (i : ℤ) (j : ℤ) : i.gcd j = i.natAbs.gcd j.natAbs

theorem Int.coe_nat_gcd (m : ℕ) (n : ℕ) : (↑m).gcd ↑n = m.gcd n

def Int.gcdA : ℤ → ℤ → ℤ

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

Equations

• x✝.gcdA x = match x✝, x with | Int.ofNat m, n => m.gcdA n.natAbs | Int.negSucc m, n => -m.succ.gcdA n.natAbs

def Int.gcdB : ℤ → ℤ → ℤ

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

Equations

• x✝.gcdB x = match x✝, x with | m, Int.ofNat n => m.natAbs.gcdB n | m, Int.negSucc n => -m.natAbs.gcdB n.succ

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.natAbs_ediv (a : ℤ) (b : ℤ) (H : b ∣ a) : (a / b).natAbs = a.natAbs / b.natAbs

theorem Int.dvd_of_mul_dvd_mul_left {i : ℤ} {j : ℤ} {k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) : i ∣ j

special case of mul_dvd_mul_iff_right for ℤ. Duplicated here to keep simple imports for this file.

theorem Int.dvd_of_mul_dvd_mul_right {i : ℤ} {j : ℤ} {k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) : i ∣ j

special case of mul_dvd_mul_iff_right for ℤ. Duplicated here to keep simple imports for this file.

theorem Int.lcm_def (i : ℤ) (j : ℤ) : i.lcm j = i.natAbs.lcm j.natAbs

theorem Int.coe_nat_lcm (m : ℕ) (n : ℕ) : (↑m).lcm ↑n = m.lcm n

theorem Int.dvd_gcd {i : ℤ} {j : ℤ} {k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) : k ∣ ↑(i.gcd j)

theorem Int.gcd_mul_lcm (i : ℤ) (j : ℤ) : i.gcd j * i.lcm j = (i * j).natAbs

theorem Int.gcd_comm (i : ℤ) (j : ℤ) : i.gcd j = j.gcd i

theorem Int.gcd_assoc (i : ℤ) (j : ℤ) (k : ℤ) : (↑(i.gcd j)).gcd k = i.gcd ↑(j.gcd k)

@[simp]

theorem Int.gcd_self (i : ℤ) : i.gcd i = i.natAbs

@[simp]

theorem Int.gcd_zero_left (i : ℤ) : Int.gcd 0 i = i.natAbs

@[simp]

theorem Int.gcd_zero_right (i : ℤ) : i.gcd 0 = i.natAbs

theorem Int.gcd_mul_left (i : ℤ) (j : ℤ) (k : ℤ) : (i * j).gcd (i * k) = i.natAbs * j.gcd k

theorem Int.gcd_mul_right (i : ℤ) (j : ℤ) (k : ℤ) : (i * j).gcd (k * j) = i.gcd k * j.natAbs

theorem Int.gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < i.gcd j

theorem Int.gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < i.gcd j

theorem Int.gcd_eq_zero_iff {i : ℤ} {j : ℤ} : i.gcd j = 0 ↔ i = 0 ∧ j = 0

theorem Int.gcd_pos_iff {i : ℤ} {j : ℤ} : 0 < i.gcd j ↔ i ≠ 0 ∨ j ≠ 0

theorem Int.gcd_div {i : ℤ} {j : ℤ} {k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) : (i / k).gcd (j / k) = i.gcd j / k.natAbs

theorem Int.gcd_div_gcd_div_gcd {i : ℤ} {j : ℤ} (H : 0 < i.gcd j) : (i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1

theorem Int.gcd_dvd_gcd_of_dvd_left {i : ℤ} {k : ℤ} (j : ℤ) (H : i ∣ k) : i.gcd j ∣ k.gcd j

theorem Int.gcd_dvd_gcd_of_dvd_right {i : ℤ} {k : ℤ} (j : ℤ) (H : i ∣ k) : j.gcd i ∣ j.gcd k

theorem Int.gcd_dvd_gcd_mul_left (i : ℤ) (j : ℤ) (k : ℤ) : i.gcd j ∣ (k * i).gcd j

theorem Int.gcd_dvd_gcd_mul_right (i : ℤ) (j : ℤ) (k : ℤ) : i.gcd j ∣ (i * k).gcd j

theorem Int.gcd_dvd_gcd_mul_left_right (i : ℤ) (j : ℤ) (k : ℤ) : i.gcd j ∣ i.gcd (k * j)

theorem Int.gcd_dvd_gcd_mul_right_right (i : ℤ) (j : ℤ) (k : ℤ) : i.gcd j ∣ i.gcd (j * k)

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.gcd_eq_left {i : ℤ} {j : ℤ} (H : i ∣ j) : i.gcd j = i.natAbs

theorem Int.gcd_eq_right {i : ℤ} {j : ℤ} (H : j ∣ i) : i.gcd j = j.natAbs

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.pow_dvd_pow_iff {m : ℤ} {n : ℤ} {k : ℕ} (k0 : k ≠ 0) : m ^ k ∣ n ^ k ↔ m ∣ n

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

lcm

theorem Int.lcm_comm (i : ℤ) (j : ℤ) : i.lcm j = j.lcm i

theorem Int.lcm_assoc (i : ℤ) (j : ℤ) (k : ℤ) : (↑(i.lcm j)).lcm k = i.lcm ↑(j.lcm k)

@[simp]

theorem Int.lcm_zero_left (i : ℤ) : Int.lcm 0 i = 0

@[simp]

theorem Int.lcm_zero_right (i : ℤ) : i.lcm 0 = 0

@[simp]

theorem Int.lcm_one_left (i : ℤ) : Int.lcm 1 i = i.natAbs

@[simp]

theorem Int.lcm_one_right (i : ℤ) : i.lcm 1 = i.natAbs

theorem Int.lcm_dvd {i : ℤ} {j : ℤ} {k : ℤ} : i ∣ k → j ∣ k → ↑(i.lcm j) ∣ k

theorem Int.lcm_mul_left {m : ℤ} {n : ℤ} {k : ℤ} : (m * n).lcm (m * k) = m.natAbs * n.lcm k

theorem Int.lcm_mul_right {m : ℤ} {n : ℤ} {k : ℤ} : (m * n).lcm (k * n) = m.lcm k * n.natAbs

theorem gcd_nsmul_eq_zero {M : Type u_1} [AddMonoid M] (x : M) {m : ℕ} {n : ℕ} (hm : m • x = 0) (hn : n • x = 0) : m.gcd n • x = 0

theorem pow_gcd_eq_one {M : Type u_1} [Monoid M] (x : M) {m : ℕ} {n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) : x ^ m.gcd n = 1

theorem Commute.pow_eq_pow_iff_of_coprime {α : Type u_1} [GroupWithZero α] {a : α} {b : α} {m : ℕ} {n : ℕ} (hab : Commute a b) (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ (c : α), a = c ^ n ∧ b = c ^ m

theorem pow_eq_pow_iff_of_coprime {α : Type u_1} [CommGroupWithZero α] {a : α} {b : α} {m : ℕ} {n : ℕ} (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ (c : α), a = c ^ n ∧ b = c ^ m

theorem pow_mem_range_pow_of_coprime {α : Type u_1} [CommGroupWithZero α] {m : ℕ} {n : ℕ} (hmn : m.Coprime n) (a : α) : (a ^ m ∈ Set.range fun (x : α) => x ^ n) ↔ a ∈ Set.range fun (x : α) => x ^ n