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. gcd_a x y and gcd_b 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 * gcd_a x y + y * gcd_b x y.

Tags

Bézout's lemma, Bezout's lemma

Extended Euclidean algorithm

ink

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

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

Equations

• Nat.xgcdAux 0 x x x x x = (x, x, x)
• Nat.xgcdAux (Nat.succ k) x x x x x = let_fun this := (_ : x % Nat.succ k < Nat.succ k); let q := x / Nat.succ k; Nat.xgcdAux (x % Nat.succ k) (x - ↑q * x) (x - ↑q * x) (Nat.succ k) x x

ink

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

ink

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

ink

@[simp]

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

ink

theorem Nat.xgcd_aux_rec {r : ℕ} {s : ℤ} {t : ℤ} {r' : ℕ} {s' : ℤ} {t' : ℤ} (h : 0 < r) : Nat.xgcdAux r s t r' s' t' = Nat.xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

ink

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

• Nat.xgcd x y = (Nat.xgcdAux x 1 0 y 0 1).snd

ink

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

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

Equations

• Nat.gcdA x y = (Nat.xgcd x y).fst

ink

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

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

Equations

• Nat.gcdB x y = (Nat.xgcd x y).snd

ink

@[simp]

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

ink

@[simp]

theorem Nat.gcdB_zero_left {s : ℕ} : Nat.gcdB 0 s = 1

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Nat.xgcd_aux_fst (x : ℕ) (y : ℕ) (s : ℤ) (t : ℤ) (s' : ℤ) (t' : ℤ) : (Nat.xgcdAux x s t y s' t').fst = Nat.gcd x y

ink

theorem Nat.xgcd_aux_val (x : ℕ) (y : ℕ) : Nat.xgcdAux x 1 0 y 0 1 = (Nat.gcd x y, Nat.xgcd x y)

ink

theorem Nat.xgcd_val (x : ℕ) (y : ℕ) : Nat.xgcd x y = (Nat.gcdA x y, Nat.gcdB x y)

ink

theorem Nat.xgcd_aux_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 (Nat.xgcdAux r s t r' s' t')

ink

theorem Nat.gcd_eq_gcd_ab (x : ℕ) (y : ℕ) : ↑(Nat.gcd x y) = ↑x * Nat.gcdA x y + ↑y * Nat.gcdB x 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.

ink

theorem Nat.exists_mul_emod_eq_gcd {k : ℕ} {n : ℕ} (hk : Nat.gcd n k < k) : ∃ m, n * m % k = Nat.gcd n k

ink

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

Divisibility over ℤ

ink

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

ink

def Int.gcdA : ℤ → ℤ → ℤ

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

Equations

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

ink

def Int.gcdB : ℤ → ℤ → ℤ

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

Equations

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

ink

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

Bézout's lemma

ink

theorem Int.natAbs_ediv (a : ℤ) (b : ℤ) (H : b ∣ a) : Int.natAbs (a / b) = Int.natAbs a / Int.natAbs b

ink

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

ink

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

ink

def Int.lcm (i : ℤ) (j : ℤ) : ℕ

ℤ specific version of least common multiple.

Equations

• Int.lcm i j = Nat.lcm (Int.natAbs i) (Int.natAbs j)

ink

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

ink

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

ink

theorem Int.gcd_dvd_left (i : ℤ) (j : ℤ) : ↑(Int.gcd i j) ∣ i

ink

theorem Int.gcd_dvd_right (i : ℤ) (j : ℤ) : ↑(Int.gcd i j) ∣ j

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Int.gcd_one_left (i : ℤ) : Int.gcd 1 i = 1

ink

@[simp]

theorem Int.gcd_one_right (i : ℤ) : Int.gcd i 1 = 1

ink

@[simp]

theorem Int.gcd_neg_right {x : ℤ} {y : ℤ} : Int.gcd x (-y) = Int.gcd x y

ink

@[simp]

theorem Int.gcd_neg_left {x : ℤ} {y : ℤ} : Int.gcd (-x) y = Int.gcd x y

ink

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

ink

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

ink

theorem Int.gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < Int.gcd i j

ink

theorem Int.gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < Int.gcd i j

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Int.exists_gcd_one {m : ℤ} {n : ℤ} (H : 0 < Int.gcd m n) : ∃ m' n', Int.gcd m' n' = 1 ∧ m = m' * ↑(Int.gcd m n) ∧ n = n' * ↑(Int.gcd m n)

ink

theorem Int.exists_gcd_one' {m : ℤ} {n : ℤ} (H : 0 < Int.gcd m n) : ∃ g m' n', 0 < g ∧ Int.gcd m' n' = 1 ∧ m = m' * ↑g ∧ n = n' * ↑g

ink

theorem Int.pow_dvd_pow_iff {m : ℤ} {n : ℤ} {k : ℕ} (k0 : 0 < k) : m ^ k ∣ n ^ k ↔ m ∣ n

ink

theorem Int.gcd_dvd_iff {a : ℤ} {b : ℤ} {n : ℕ} : Int.gcd a b ∣ n ↔ ∃ x y, ↑n = a * x + b * y

ink

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 = ↑(Int.gcd a b)

ink

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

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

ink

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

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

ink

theorem Int.gcd_least_linear {a : ℤ} {b : ℤ} (ha : a ≠ 0) : IsLeast { n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y } (Int.gcd a 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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Int.lcm_self (i : ℤ) : Int.lcm i i = Int.natAbs i

ink

theorem Int.dvd_lcm_left (i : ℤ) (j : ℤ) : i ∣ ↑(Int.lcm i j)

ink

theorem Int.dvd_lcm_right (i : ℤ) (j : ℤ) : j ∣ ↑(Int.lcm i j)

ink

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

ink

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

ink

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

GCD prover