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.

Extended Euclidean algorithm

source

def nat.xgcd_aux :

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

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

Equations

_x.succ.xgcd_aux s t r' s' t' = let q : ℕ := r' / _x.succ in (r' % _x.succ).xgcd_aux (s' - ↑q * s) (t' - ↑q * t) _x.succ s t
0.xgcd_aux s t r' s' t' = (r', s', t')

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' : ℤ} :

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 :

ℕ → ℕ → ℤ × ℤ

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.xgcd_aux 1 0 y 0 1).snd

source

def nat.gcd_a :

ℕ → ℕ → ℤ

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

Equations

x.gcd_a y = (x.xgcd y).fst

source

def nat.gcd_b :

ℕ → ℕ → ℤ

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

Equations

x.gcd_b y = (x.xgcd y).snd

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' : ℤ} :

P x y (r, s, t) → 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.