mathlib3 documentation

data.int.gcd

Extended GCD and divisibility over ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Main statements #

Tags #

Bézout's lemma, Bezout's lemma

Extended Euclidean algorithm #

source
def nat.xgcd_aux  :
ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ

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

Equations
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' : ℤ} (h : 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 (x y : ℕ) :
ℤ × ℤ

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

Equations
source
def nat.gcd_a (x y : ℕ) :
ℤ

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

Equations
source
def nat.gcd_b (x y : ℕ) :
ℤ

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

Equations
source
@[simp]
theorem nat.gcd_a_zero_left {s : ℕ} :
0.gcd_a s = 0
source
@[simp]
theorem nat.gcd_b_zero_left {s : ℕ} :
0.gcd_b s = 1
source
@[simp]
theorem nat.gcd_a_zero_right {s : ℕ} (h : s ≠ 0) :
s.gcd_a 0 = 1
source
@[simp]
theorem nat.gcd_b_zero_right {s : ℕ} (h : s ≠ 0) :
s.gcd_b 0 = 0
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.

source
theorem nat.exists_mul_mod_eq_gcd {k n : ℕ} (hk : n.gcd k < k) :
∃ (m : ℕ), n * m % k = n.gcd k
source
theorem nat.exists_mul_mod_eq_one_of_coprime {k n : ℕ} (hkn : n.coprime k) (hk : 1 < k) :
∃ (m : ℕ), n * m % k = 1

Divisibility over ℤ #

source
@[protected]
theorem int.coe_nat_gcd (m n : ℕ) :
↑m.gcd ↑n = m.gcd n
source
def int.gcd_a  :
ℤ → ℤ → ℤ

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

Equations
source
def int.gcd_b  :
ℤ → ℤ → ℤ

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

Equations
source
theorem int.gcd_eq_gcd_ab (x y : ℤ) :
↑(x.gcd y) = x * x.gcd_a y + y * x.gcd_b y

Bézout's lemma

source
theorem int.nat_abs_div (a b : ℤ) (H : b ∣ a) :
(a / b).nat_abs = a.nat_abs / b.nat_abs
source
theorem int.dvd_of_mul_dvd_mul_left {i j k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) :
i ∣ j
source
theorem int.dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) :
i ∣ j
source
def int.lcm (i j : ℤ) :
ℕ

ℤ specific version of least common multiple.

Equations
source
theorem int.lcm_def (i j : ℤ) :
i.lcm j = i.nat_abs.lcm j.nat_abs
source
@[protected]
theorem int.coe_nat_lcm (m n : ℕ) :
↑m.lcm ↑n = m.lcm n
source
theorem int.gcd_dvd_left (i j : ℤ) :
↑(i.gcd j) ∣ i
source
theorem int.gcd_dvd_right (i j : ℤ) :
↑(i.gcd j) ∣ j
source
theorem int.dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) :
k ∣ ↑(i.gcd j)
source
theorem int.gcd_mul_lcm (i j : ℤ) :
i.gcd j * i.lcm j = (i * j).nat_abs
source
theorem int.gcd_comm (i j : ℤ) :
i.gcd j = j.gcd i
source
theorem int.gcd_assoc (i j k : ℤ) :
↑(i.gcd j).gcd k = i.gcd ↑(j.gcd k)
source
@[simp]
theorem int.gcd_self (i : ℤ) :
i.gcd i = i.nat_abs
source
@[simp]
theorem int.gcd_zero_left (i : ℤ) :
0.gcd i = i.nat_abs
source
@[simp]
theorem int.gcd_zero_right (i : ℤ) :
i.gcd 0 = i.nat_abs
source
@[simp]
theorem int.gcd_one_left (i : ℤ) :
1.gcd i = 1
source
@[simp]
theorem int.gcd_one_right (i : ℤ) :
i.gcd 1 = 1
source
@[simp]
theorem int.gcd_neg_right {x y : ℤ} :
x.gcd (-y) = x.gcd y
source
@[simp]
theorem int.gcd_neg_left {x y : ℤ} :
(-x).gcd y = x.gcd y
source
theorem int.gcd_mul_left (i j k : ℤ) :
(i * j).gcd (i * k) = i.nat_abs * j.gcd k
source
theorem int.gcd_mul_right (i j k : ℤ) :
(i * j).gcd (k * j) = i.gcd k * j.nat_abs
source
theorem int.gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) :
0 < i.gcd j
source
theorem int.gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) :
0 < i.gcd j
source
theorem int.gcd_eq_zero_iff {i j : ℤ} :
i.gcd j = 0 ↔ i = 0 ∧ j = 0
source
theorem int.gcd_pos_iff {i j : ℤ} :
0 < i.gcd j ↔ i ≠ 0 ∨ j ≠ 0
source
theorem int.gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
(i / k).gcd (j / k) = i.gcd j / k.nat_abs
source
theorem int.gcd_div_gcd_div_gcd {i j : ℤ} (H : 0 < i.gcd j) :
(i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1
source
theorem int.gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) :
i.gcd j ∣ k.gcd j
source
theorem int.gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) :
j.gcd i ∣ j.gcd k
source
theorem int.gcd_dvd_gcd_mul_left (i j k : ℤ) :
i.gcd j ∣ (k * i).gcd j
source
theorem int.gcd_dvd_gcd_mul_right (i j k : ℤ) :
i.gcd j ∣ (i * k).gcd j
source
theorem int.gcd_dvd_gcd_mul_left_right (i j k : ℤ) :
i.gcd j ∣ i.gcd (k * j)
source
theorem int.gcd_dvd_gcd_mul_right_right (i j k : ℤ) :
i.gcd j ∣ i.gcd (j * k)
source
theorem int.gcd_eq_left {i j : ℤ} (H : i ∣ j) :
i.gcd j = i.nat_abs
source
theorem int.gcd_eq_right {i j : ℤ} (H : j ∣ i) :
i.gcd j = j.nat_abs
source
theorem int.ne_zero_of_gcd {x y : ℤ} (hc : x.gcd y ≠ 0) :
x ≠ 0 ∨ y ≠ 0
source
theorem int.exists_gcd_one {m n : ℤ} (H : 0 < m.gcd n) :
∃ (m' n' : ℤ), m'.gcd n' = 1 ∧ m = m' * ↑(m.gcd n) ∧ n = n' * ↑(m.gcd n)
source
theorem int.exists_gcd_one' {m n : ℤ} (H : 0 < m.gcd n) :
∃ (g : ℕ) (m' n' : ℤ), 0 < g ∧ m'.gcd n' = 1 ∧ m = m' * ↑g ∧ n = n' * ↑g
source
theorem int.pow_dvd_pow_iff {m n : ℤ} {k : ℕ} (k0 : 0 < k) :
m ^ k ∣ n ^ k ↔ m ∣ n
source
theorem int.gcd_dvd_iff {a b : ℤ} {n : ℕ} :
a.gcd b ∣ n ↔ ∃ (x y : ℤ), ↑n = a * x + b * y
source
theorem int.gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ (e : ℤ), e ∣ a → e ∣ b → e ∣ d) :
d = ↑(a.gcd b)
source
theorem int.dvd_of_dvd_mul_left_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : a.gcd c = 1) :
a ∣ b

Euclid's lemma: if a ∣ b * c and gcd a c = 1 then a ∣ b. Compare with is_coprime.dvd_of_dvd_mul_left and unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_factors

source
theorem int.dvd_of_dvd_mul_right_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : a.gcd b = 1) :
a ∣ c

Euclid's lemma: if a ∣ b * c and gcd a b = 1 then a ∣ c. Compare with is_coprime.dvd_of_dvd_mul_right and unique_factorization_monoid.dvd_of_dvd_mul_right_of_no_prime_factors

source
theorem int.gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :
is_least {n : ℕ | 0 < n ∧ ∃ (x y : ℤ), ↑n = a * x + b * y} (a.gcd b)

For nonzero integers a and b, gcd a b is the smallest positive natural number that can be written in the form a * x + b * y for some pair of integers x and y

lcm #

source
theorem int.lcm_comm (i j : ℤ) :
i.lcm j = j.lcm i
source
theorem int.lcm_assoc (i j k : ℤ) :
↑(i.lcm j).lcm k = i.lcm ↑(j.lcm k)
source
@[simp]
theorem int.lcm_zero_left (i : ℤ) :
0.lcm i = 0
source
@[simp]
theorem int.lcm_zero_right (i : ℤ) :
i.lcm 0 = 0
source
@[simp]
theorem int.lcm_one_left (i : ℤ) :
1.lcm i = i.nat_abs
source
@[simp]
theorem int.lcm_one_right (i : ℤ) :
i.lcm 1 = i.nat_abs
source
@[simp]
theorem int.lcm_self (i : ℤ) :
i.lcm i = i.nat_abs
source
theorem int.dvd_lcm_left (i j : ℤ) :
i ∣ ↑(i.lcm j)
source
theorem int.dvd_lcm_right (i j : ℤ) :
j ∣ ↑(i.lcm j)
source
theorem int.lcm_dvd {i j k : ℤ} :
i ∣ k → j ∣ k → ↑(i.lcm j) ∣ k
source
theorem pow_gcd_eq_one {M : Type u_1} [monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
x ^ m.gcd n = 1
source
theorem gcd_nsmul_eq_zero {M : Type u_1} [add_monoid M] (x : M) {m n : ℕ} (hm : m • x = 0) (hn : n • x = 0) :
m.gcd n • x = 0

GCD prover #

source
theorem tactic.norm_num.int_gcd_helper' {d : ℕ} {x y a b : ℤ} (h₁ : ↑d ∣ x) (h₂ : ↑d ∣ y) (h₃ : x * a + y * b = ↑d) :
x.gcd y = d
source
theorem tactic.norm_num.nat_gcd_helper_dvd_left (x y a : ℕ) (h : x * a = y) :
x.gcd y = x
source
theorem tactic.norm_num.nat_gcd_helper_dvd_right (x y a : ℕ) (h : y * a = x) :
x.gcd y = y
source
theorem tactic.norm_num.nat_gcd_helper_2 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y) (hx : x * a = tx) (hy : y * b = ty) (h : ty + d = tx) :
x.gcd y = d
source
theorem tactic.norm_num.nat_gcd_helper_1 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y) (hx : x * a = tx) (hy : y * b = ty) (h : tx + d = ty) :
x.gcd y = d
source
theorem tactic.norm_num.nat_lcm_helper (x y d m n : ℕ) (hd : x.gcd y = d) (d0 : 0 < d) (xy : x * y = n) (dm : d * m = n) :
x.lcm y = m
source
theorem tactic.norm_num.nat_coprime_helper_zero_left (x : ℕ) (h : 1 < x) :
¬0.coprime x
source
theorem tactic.norm_num.nat_coprime_helper_zero_right (x : ℕ) (h : 1 < x) :
¬x.coprime 0
source
theorem tactic.norm_num.nat_coprime_helper_1 (x y a b tx ty : ℕ) (hx : x * a = tx) (hy : y * b = ty) (h : tx + 1 = ty) :
x.coprime y
source
theorem tactic.norm_num.nat_coprime_helper_2 (x y a b tx ty : ℕ) (hx : x * a = tx) (hy : y * b = ty) (h : ty + 1 = tx) :
x.coprime y
source
theorem tactic.norm_num.nat_not_coprime_helper (d x y u v : ℕ) (hu : d * u = x) (hv : d * v = y) (h : 1 < d) :
¬x.coprime y
source
theorem tactic.norm_num.int_gcd_helper (x y : ℤ) (nx ny d : ℕ) (hx : ↑nx = x) (hy : ↑ny = y) (h : nx.gcd ny = d) :
x.gcd y = d
source
theorem tactic.norm_num.int_gcd_helper_neg_left (x y : ℤ) (d : ℕ) (h : x.gcd y = d) :
(-x).gcd y = d
source
theorem tactic.norm_num.int_gcd_helper_neg_right (x y : ℤ) (d : ℕ) (h : x.gcd y = d) :
x.gcd (-y) = d
source
theorem tactic.norm_num.int_lcm_helper (x y : ℤ) (nx ny d : ℕ) (hx : ↑nx = x) (hy : ↑ny = y) (h : nx.lcm ny = d) :
x.lcm y = d
source
theorem tactic.norm_num.int_lcm_helper_neg_left (x y : ℤ) (d : ℕ) (h : x.lcm y = d) :
(-x).lcm y = d
source
theorem tactic.norm_num.int_lcm_helper_neg_right (x y : ℤ) (d : ℕ) (h : x.lcm y = d) :
x.lcm (-y) = d
source
meta def tactic.norm_num.prove_gcd_nat (c : tactic.instance_cache) (ex ey : expr) :
tactic (tactic.instance_cache × expr × expr)

Evaluates the nat.gcd function.

source
meta def tactic.norm_num.prove_lcm_nat (c : tactic.instance_cache) (ex ey : expr) :
tactic (tactic.instance_cache × expr × expr)

Evaluates the nat.lcm function.

source
meta def tactic.norm_num.prove_gcd_int (zc nc : tactic.instance_cache) :
expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Evaluates the int.gcd function.

source
meta def tactic.norm_num.prove_lcm_int (zc nc : tactic.instance_cache) :
expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

Evaluates the int.lcm function.

source
meta def tactic.norm_num.prove_coprime_nat (c : tactic.instance_cache) (ex ey : expr) :
tactic (tactic.instance_cache × (expr ⊕ expr))

Evaluates the nat.coprime function.

source
meta def tactic.norm_num.eval_gcd  :
expr → tactic (expr × expr)

Evaluates the gcd, lcm, and coprime functions.