Documentation

Mathlib.Data.Int.GCD

Extended GCD and divisibility over ℤ #

Main definitions #

Main statements #

Tags #

Bézout's lemma, Bezout's lemma

Extended Euclidean algorithm #

@[irreducible]
def Nat.xgcdAux :
× ×

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

Equations
  • Nat.xgcdAux 0 x✝³ x✝² x✝¹ x✝ x = (x✝¹, x✝, x)
  • k.succ.xgcdAux x✝³ x✝² x✝¹ x✝ x = (x✝¹ % k.succ).xgcdAux (x✝ - (x✝¹ / k.succ) * x✝³) (x - (x✝¹ / k.succ) * x✝²) k.succ x✝³ x✝²
Instances For
    @[simp]
    theorem Nat.xgcd_zero_left {s : } {t : } {r' : } {s' : } {t' : } :
    Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
    theorem Nat.xgcdAux_rec {r : } {s : } {t : } {r' : } {s' : } {t' : } (h : 0 < r) :
    r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - r' / r * s) (t' - r' / r * t) r s t
    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
    • x.xgcd y = (x.xgcdAux 1 0 y 0 1).2
    Instances For
      def Nat.gcdA (x : ) (y : ) :

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

      Equations
      • x.gcdA y = (x.xgcd y).1
      Instances For
        def Nat.gcdB (x : ) (y : ) :

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

        Equations
        • x.gcdB y = (x.xgcd y).2
        Instances For
          @[simp]
          theorem Nat.gcdA_zero_left {s : } :
          Nat.gcdA 0 s = 0
          @[simp]
          theorem Nat.gcdB_zero_left {s : } :
          Nat.gcdB 0 s = 1
          @[simp]
          theorem Nat.gcdA_zero_right {s : } (h : s 0) :
          s.gcdA 0 = 1
          @[simp]
          theorem Nat.gcdB_zero_right {s : } (h : s 0) :
          s.gcdB 0 = 0
          @[simp]
          theorem Nat.xgcdAux_fst (x : ) (y : ) (s : ) (t : ) (s' : ) (t' : ) :
          (x.xgcdAux s t y s' t').1 = x.gcd y
          theorem Nat.xgcdAux_val (x : ) (y : ) :
          x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
          theorem Nat.xgcd_val (x : ) (y : ) :
          x.xgcd y = (x.gcdA y, x.gcdB y)
          theorem Nat.xgcdAux_P (x : ) (y : ) {r : } {r' : } {s : } {t : } {s' : } {t' : } :
          Nat.P x y (r, s, t)Nat.P x y (r', s', t')Nat.P x y (r.xgcdAux s t r' s' t')
          theorem Nat.gcd_eq_gcd_ab (x : ) (y : ) :
          (x.gcd y) = x * x.gcdA y + y * x.gcdB 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.

          theorem Nat.exists_mul_emod_eq_gcd {k : } {n : } (hk : n.gcd k < k) :
          ∃ (m : ), n * m % k = n.gcd k
          theorem Nat.exists_mul_emod_eq_one_of_coprime {k : } {n : } (hkn : n.Coprime k) (hk : 1 < k) :
          ∃ (m : ), n * m % k = 1

          Divisibility over ℤ #

          theorem Int.gcd_def (i : ) (j : ) :
          i.gcd j = i.natAbs.gcd j.natAbs
          @[simp]
          theorem Int.gcd_natCast_natCast (m : ) (n : ) :
          (↑m).gcd n = m.gcd n
          @[deprecated Int.gcd_natCast_natCast]
          theorem Int.coe_nat_gcd (m : ) (n : ) :
          (↑m).gcd n = m.gcd n

          Alias of Int.gcd_natCast_natCast.

          def Int.gcdA :

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

          Equations
          Instances For
            def Int.gcdB :

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

            Equations
            Instances For
              theorem Int.gcd_eq_gcd_ab (x : ) (y : ) :
              (x.gcd y) = x * x.gcdA y + y * x.gcdB y

              Bézout's lemma

              theorem Int.lcm_def (i : ) (j : ) :
              i.lcm j = i.natAbs.lcm j.natAbs
              theorem Int.coe_nat_lcm (m : ) (n : ) :
              (↑m).lcm n = m.lcm n
              theorem Int.dvd_gcd {i : } {j : } {k : } (h1 : k i) (h2 : k j) :
              k (i.gcd j)
              theorem Int.gcd_mul_lcm (i : ) (j : ) :
              i.gcd j * i.lcm j = (i * j).natAbs
              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.natAbs
              @[simp]
              theorem Int.gcd_zero_left (i : ) :
              Int.gcd 0 i = i.natAbs
              @[simp]
              theorem Int.gcd_zero_right (i : ) :
              i.gcd 0 = i.natAbs
              theorem Int.gcd_mul_left (i : ) (j : ) (k : ) :
              (i * j).gcd (i * k) = i.natAbs * j.gcd k
              theorem Int.gcd_mul_right (i : ) (j : ) (k : ) :
              (i * j).gcd (k * j) = i.gcd k * j.natAbs
              theorem Int.gcd_pos_of_ne_zero_left {i : } (j : ) (hi : i 0) :
              0 < i.gcd j
              theorem Int.gcd_pos_of_ne_zero_right (i : ) {j : } (hj : j 0) :
              0 < i.gcd j
              theorem Int.gcd_eq_zero_iff {i : } {j : } :
              i.gcd j = 0 i = 0 j = 0
              theorem Int.gcd_pos_iff {i : } {j : } :
              0 < i.gcd j i 0 j 0
              theorem Int.gcd_div {i : } {j : } {k : } (H1 : k i) (H2 : k j) :
              (i / k).gcd (j / k) = i.gcd j / k.natAbs
              theorem Int.gcd_div_gcd_div_gcd {i : } {j : } (H : 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 : ) (H : i k) :
              i.gcd j k.gcd j
              theorem Int.gcd_dvd_gcd_of_dvd_right {i : } {k : } (j : ) (H : i k) :
              j.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_one_of_gcd_mul_right_eq_one_left {a : } {m : } {n : } (h : a.gcd (m * n) = 1) :
              a.gcd m = 1

              If gcd a (m * n) = 1, then gcd a m = 1.

              theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_right {a : } {m : } {n : } (h : a.gcd (m * n) = 1) :
              a.gcd n = 1

              If gcd a (m * n) = 1, then gcd a n = 1.

              theorem Int.gcd_eq_left {i : } {j : } (H : i j) :
              i.gcd j = i.natAbs
              theorem Int.gcd_eq_right {i : } {j : } (H : j i) :
              i.gcd j = j.natAbs
              theorem Int.ne_zero_of_gcd {x : } {y : } (hc : x.gcd y 0) :
              x 0 y 0
              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)
              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
              theorem Int.pow_dvd_pow_iff {m : } {n : } {k : } (k0 : k 0) :
              m ^ k n ^ k m n
              theorem Int.gcd_dvd_iff {a : } {b : } {n : } :
              a.gcd b n ∃ (x : ), ∃ (y : ), n = a * x + b * y
              theorem Int.gcd_greatest {a : } {b : } {d : } (hd_pos : 0 d) (hda : d a) (hdb : d b) (hd : ∀ (e : ), e ae be d) :
              d = (a.gcd b)
              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 IsCoprime.dvd_of_dvd_mul_left and UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors

              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 IsCoprime.dvd_of_dvd_mul_right and UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors

              theorem Int.gcd_least_linear {a : } {b : } (ha : a 0) :
              IsLeast {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 #

              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 : ) :
              Int.lcm 0 i = 0
              @[simp]
              theorem Int.lcm_zero_right (i : ) :
              i.lcm 0 = 0
              @[simp]
              theorem Int.lcm_one_left (i : ) :
              Int.lcm 1 i = i.natAbs
              @[simp]
              theorem Int.lcm_one_right (i : ) :
              i.lcm 1 = i.natAbs
              theorem Int.lcm_dvd {i : } {j : } {k : } :
              i kj k(i.lcm j) k
              theorem Int.lcm_mul_left {m : } {n : } {k : } :
              (m * n).lcm (m * k) = m.natAbs * n.lcm k
              theorem Int.lcm_mul_right {m : } {n : } {k : } :
              (m * n).lcm (k * n) = m.lcm k * n.natAbs
              theorem gcd_nsmul_eq_zero {M : Type u_1} [AddMonoid M] (x : M) {m : } {n : } (hm : m x = 0) (hn : n x = 0) :
              m.gcd n x = 0
              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
              theorem Commute.pow_eq_pow_iff_of_coprime {α : Type u_1} [GroupWithZero α] {a : α} {b : α} {m : } {n : } (hab : Commute a b) (hmn : m.Coprime n) :
              a ^ m = b ^ n ∃ (c : α), a = c ^ n b = c ^ m
              theorem pow_eq_pow_iff_of_coprime {α : Type u_1} [CommGroupWithZero α] {a : α} {b : α} {m : } {n : } (hmn : m.Coprime n) :
              a ^ m = b ^ n ∃ (c : α), a = c ^ n b = c ^ m
              theorem pow_mem_range_pow_of_coprime {α : Type u_1} [CommGroupWithZero α] {m : } {n : } (hmn : m.Coprime n) (a : α) :
              (a ^ m Set.range fun (x : α) => x ^ n) a Set.range fun (x : α) => x ^ n