mathlib documentation

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

def int.lcm  :

ℤ specific version of least common multiple.

Equations
theorem int.lcm_def (i j : ) :

theorem int.gcd_dvd_left (i j : ) :
(i.gcd j) i

theorem int.gcd_dvd_right (i j : ) :
(i.gcd j) j

theorem int.dvd_gcd {i j k : } :
k ik jk (i.gcd j)

theorem int.gcd_mul_lcm (i j : ) :
(i.gcd j) * i.lcm j = (i * j).nat_abs

theorem int.gcd_comm (i j : ) :
i.gcd j = j.gcd i

theorem int.gcd_assoc (i j k : ) :
(i.gcd j).gcd k = i.gcd (j.gcd k)

@[simp]
theorem int.gcd_self (i : ) :
i.gcd i = i.nat_abs

@[simp]
theorem int.gcd_zero_left (i : ) :
0.gcd i = i.nat_abs

@[simp]
theorem int.gcd_zero_right (i : ) :
i.gcd 0 = i.nat_abs

@[simp]
theorem int.gcd_one_left (i : ) :
1.gcd i = 1

@[simp]
theorem int.gcd_one_right (i : ) :
i.gcd 1 = 1

theorem int.gcd_mul_left (i j k : ) :
(i * j).gcd (i * k) = (i.nat_abs) * j.gcd k

theorem int.gcd_mul_right (i j k : ) :
(i * j).gcd (k * j) = (i.gcd k) * j.nat_abs

theorem int.gcd_pos_of_non_zero_left {i : } (j : ) :
i 00 < i.gcd j

theorem int.gcd_pos_of_non_zero_right (i : ) {j : } :
j 00 < i.gcd j

theorem int.gcd_eq_zero_iff {i j : } :
i.gcd j = 0 i = 0 j = 0

theorem int.gcd_div {i j k : } :
k ik j(i / k).gcd (j / k) = i.gcd j / k.nat_abs

theorem int.gcd_div_gcd_div_gcd {i j : } :
0 < i.gcd j(i / (i.gcd j)).gcd (j / (i.gcd j)) = 1

theorem int.gcd_dvd_gcd_of_dvd_left {i k : } (j : ) :
i ki.gcd j k.gcd j

theorem int.gcd_dvd_gcd_of_dvd_right {i k : } (j : ) :
i kj.gcd i j.gcd k

theorem int.gcd_dvd_gcd_mul_left (i j k : ) :
i.gcd j (k * i).gcd j

theorem int.gcd_dvd_gcd_mul_right (i j k : ) :
i.gcd j (i * k).gcd j

theorem int.gcd_dvd_gcd_mul_left_right (i j k : ) :
i.gcd j i.gcd (k * j)

theorem int.gcd_dvd_gcd_mul_right_right (i j k : ) :
i.gcd j i.gcd (j * k)

theorem int.gcd_eq_left {i j : } :
i ji.gcd j = i.nat_abs

theorem int.gcd_eq_right {i j : } :
j ii.gcd j = j.nat_abs

theorem int.ne_zero_of_gcd {x y : } :
x.gcd y 0x 0 y 0

theorem int.exists_gcd_one {m n : } :
0 < m.gcd n(∃ (m' n' : ), m'.gcd n' = 1 m = m' * (m.gcd n) n = n' * (m.gcd n))

theorem int.exists_gcd_one' {m n : } :
0 < m.gcd n(∃ (g : ) (m' n' : ), 0 < g m'.gcd n' = 1 m = m' * g n = n' * g)

theorem int.pow_dvd_pow_iff {m n : } {k : } :
0 < k(m ^ k n ^ k m n)

lcm

theorem int.lcm_comm (i j : ) :
i.lcm j = j.lcm i

theorem int.lcm_assoc (i j k : ) :
(i.lcm j).lcm k = i.lcm (j.lcm k)

@[simp]
theorem int.lcm_zero_left (i : ) :
0.lcm i = 0

@[simp]
theorem int.lcm_zero_right (i : ) :
i.lcm 0 = 0

@[simp]
theorem int.lcm_one_left (i : ) :
1.lcm i = i.nat_abs

@[simp]
theorem int.lcm_one_right (i : ) :
i.lcm 1 = i.nat_abs

@[simp]
theorem int.lcm_self (i : ) :
i.lcm i = i.nat_abs

theorem int.dvd_lcm_left (i j : ) :
i (i.lcm j)

theorem int.dvd_lcm_right (i j : ) :
j (i.lcm j)

theorem int.lcm_dvd {i j k : } :
i kj k(i.lcm j) k

theorem pow_gcd_eq_one {M : Type u_1} [monoid M] (x : M) {m n : } :
x ^ m = 1x ^ n = 1x ^ m.gcd n = 1