Extended GCD and divisibility over ℤ #
Main definitions #
- Given
x y : ℕ
,xgcd x y
computes the pair of integers(a, b)
such thatgcd x y = x * a + y * b
.gcd_a x y
andgcd_b x y
are defined to bea
andb
, respectively.
Main statements #
gcd_eq_gcd_ab
: Bézout's lemma, givenx 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 #
Helper function for the extended GCD algorithm (Nat.xgcd
).
theorem
Nat.xgcdAux_zero
{s : ℤ}
{t : ℤ}
{r' : ℕ}
{s' : ℤ}
{t' : ℤ}
:
Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
@[simp]
theorem
Nat.xgcd_zero_left
{s : ℤ}
{t : ℤ}
{r' : ℕ}
{s' : ℤ}
{t' : ℤ}
:
Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
theorem
Nat.exists_mul_emod_eq_one_of_coprime
{k : ℕ}
{n : ℕ}
(hkn : Nat.coprime n k)
(hk : 1 < k)
:
Divisibility over ℤ #
theorem
Int.natAbs_ediv
(a : ℤ)
(b : ℤ)
(H : b ∣ a)
:
Int.natAbs (a / b) = Int.natAbs a / Int.natAbs b