mathlib documentation

data.int.gcd

Extended GCD and divisibility over ℤ

Main definitions

Main statements

Extended Euclidean algorithm

source
def nat.xgcd_aux (a : ℕ) (a_1 a_2 : ℤ) (a_3 : ℕ) (a_4 a_5 : ℤ) :
ℕ × ℤ × ℤ

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

Equations
source
@[simp]
theorem nat.xgcd_zero_left {s t : ℤ} {r' : ℕ} {s' t' : ℤ} :
0.xgcd_aux s t r' s' t' = (r', s', t')

source
theorem nat.xgcd_aux_rec {r : ℕ} {s t : ℤ} {r' : ℕ} {s' t' : ℤ} (h : 0 < r) :
r.xgcd_aux s t r' s' t' = (r' % r).xgcd_aux (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
source
def nat.gcd_a (x y : ℕ) :
ℤ

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

Equations
source
def nat.gcd_b (x y : ℕ) :
ℤ

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

Equations
source
@[simp]
theorem nat.xgcd_aux_fst (x y : ℕ) (s t s' t' : ℤ) :
(x.xgcd_aux s t y s' t').fst = x.gcd y

source
theorem nat.xgcd_aux_val (x y : ℕ) :
x.xgcd_aux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

source
theorem nat.xgcd_val (x y : ℕ) :
x.xgcd y = (x.gcd_a y, x.gcd_b y)

source
theorem nat.xgcd_aux_P (x y : ℕ) {r r' : ℕ} {s t s' t' : ℤ} (a : P x y (r, s, t)) (a_1 : P x y (r', s', t')) :
P x y (r.xgcd_aux s t r' s' t')

source
theorem nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = (↑x) * x.gcd_a y + (↑y) * x.gcd_b 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.

Divisibility over ℤ

source
theorem int.nat_abs_div (a b : ℤ) (H : b ∣ a) :
(a / b).nat_abs = a.nat_abs / b.nat_abs

source
theorem int.nat_abs_dvd_abs_iff {i j : ℤ} :
i.nat_abs ∣ j.nat_abs ↔ i ∣ j

source
theorem int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ} (hpm : ↑(p ^ k) ∣ m) (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k + l + 1)) ∣ m * n) :
↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n

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

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

source
theorem int.prime.dvd_nat_abs_of_coe_dvd_pow_two {p : ℕ} (hp : nat.prime p) (k : ℤ) (h : ↑p ∣ k ^ 2) :
p ∣ k.nat_abs

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