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
Helper function for the extended GCD algorithm (nat.xgcd
).
Equations
Use the extended GCD algorithm to generate the a
and b
values
satisfying gcd x y = x * a + y * b
.
Equations
The extended GCD a
value in the equation gcd x y = x * a + y * b
.
Equations
The extended GCD b
value in the equation gcd x y = x * a + y * b
.
Equations
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 ℤ