mathlib documentation

data.​int.​gcd

data.​int.​gcd

Extended GCD and divisibility over ℤ

Main definitions

Main statements

Extended Euclidean algorithm

def nat.​xgcd_aux  :
× ×

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

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

theorem nat.​xgcd_aux_rec {r : } {s t : } {r' : } {s' t' : } :
0 < rr.xgcd_aux s t r' s' t' = (r' % r).xgcd_aux (s' - r' / r * s) (t' - r' / r * t) r s t

def nat.​xgcd  :
×

Use the extended GCD algorithm to generate the a and b values satisfying gcd x y = x * a + y * b.

Equations
def nat.​gcd_a  :

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

Equations
def nat.​gcd_b  :

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

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

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

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

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')

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 ℤ

theorem int.​nat_abs_div (a b : ) :
b a(a / b).nat_abs = a.nat_abs / b.nat_abs

theorem int.​succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (p_prime : nat.prime p) {m n : } {k l : } :
(p ^ k) m(p ^ l) n(p ^ (k + l + 1)) m * n(p ^ (k + 1)) m (p ^ (l + 1)) n

theorem int.​dvd_of_mul_dvd_mul_left {i j k : } :
k 0k * i k * ji j

theorem int.​dvd_of_mul_dvd_mul_right {i j k : } :
k 0i * k j * ki j

theorem int.​prime.​dvd_nat_abs_of_coe_dvd_pow_two {p : } (hp : nat.prime p) (k : ) :
p k ^ 2p k.nat_abs