# 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 #

source
@[irreducible]
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✝³

Instances For

source
@[simp]
theorem Nat.xgcd_zero_left {s t : ℤ} {r' : ℕ} {s' t' : ℤ} :
xgcdAux 0 s t r' s' t' = (r', s', t')
source
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
source
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

Instances For

source
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

Instances For

source
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

Instances For

source
@[simp]
theorem Nat.gcdA_zero_left {s : ℕ} :
gcdA 0 s = 0
source
@[simp]
theorem Nat.gcdB_zero_left {s : ℕ} :
gcdB 0 s = 1
source
@[simp]
theorem Nat.gcdA_zero_right {s : ℕ} (h : s ≠ 0) :
s.gcdA 0 = 1
source
@[simp]
theorem Nat.gcdB_zero_right {s : ℕ} (h : s ≠ 0) :
s.gcdB 0 = 0
source
@[simp]
theorem Nat.xgcdAux_fst (x y : ℕ) (s t s' t' : ℤ) :
(x.xgcdAux s t y s' t').1 = x.gcd y
source
theorem Nat.xgcdAux_val (x y : ℕ) :
x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
source
theorem Nat.xgcd_val (x y : ℕ) :
x.xgcd y = (x.gcdA y, x.gcdB y)
source
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')
source
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.

source
theorem Nat.exists_mul_emod_eq_gcd {k n : ℕ} (hk : n.gcd k < k) :
∃ (m : ℕ), n * m % k = n.gcd k
source
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 ℤ #

source
theorem Int.gcd_def (i j : ℤ) :
i.gcd j = i.natAbs.gcd j.natAbs
source
def Int.gcdA :
ℤ → ℤ → ℤ

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

Equations

- (Int.ofNat m).gcdA x✝ = m.gcdA x✝.natAbs
- (Int.negSucc m).gcdA x✝ = -m.succ.gcdA x✝.natAbs

Instances For

source
def Int.gcdB :
ℤ → ℤ → ℤ

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

Equations

- x✝.gcdB (Int.ofNat n) = x✝.natAbs.gcdB n
- x✝.gcdB (Int.negSucc n) = -x✝.natAbs.gcdB n.succ

Instances For

source
theorem Int.gcd_eq_gcd_ab (x y : ℤ) :
↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y

Bézout's lemma

source
theorem Int.lcm_def (i j : ℤ) :
i.lcm j = i.natAbs.lcm j.natAbs
source
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`.

source
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`.

source
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`.

source
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`.

source
theorem Int.ne_zero_of_gcd {x y : ℤ} (hc : x.gcd y ≠ 0) :
x ≠ 0 ∨ y ≠ 0
source
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)
source
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
source
theorem Int.gcd_dvd_iff {a b : ℤ} {n : ℕ} :
a.gcd b ∣ n ↔ ∃ (x : ℤ), ∃ (y : ℤ), ↑n = a * x + b * y
source
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)
source
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`

source
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`

source
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`

source
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
source
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
source
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
source
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
source
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