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 #

def Nat.xgcdAux :
× ×

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

Equations
Instances For
    theorem Nat.xgcdAux_zero {s : } {t : } {r' : } {s' : } {t' : } :
    Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
    theorem Nat.xgcdAux_succ {k : } {s : } {t : } {r' : } {s' : } {t' : } :
    Nat.xgcdAux (Nat.succ k) s t r' s' t' = Nat.xgcdAux (r' % Nat.succ k) (s' - r' / ↑(Nat.succ k) * s) (t' - r' / ↑(Nat.succ k) * t) (Nat.succ k) 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.xgcdAux_rec {r : } {s : } {t : } {r' : } {s' : } {t' : } (h : 0 < r) :
    Nat.xgcdAux r s t r' s' t' = Nat.xgcdAux (r' % r) (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
    Instances For
      def Nat.gcdA (x : ) (y : ) :

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

      Equations
      Instances For
        def Nat.gcdB (x : ) (y : ) :

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

        Equations
        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) :
          Nat.gcdA s 0 = 1
          @[simp]
          theorem Nat.gcdB_zero_right {s : } (h : s 0) :
          Nat.gcdB s 0 = 0
          @[simp]
          theorem Nat.xgcdAux_fst (x : ) (y : ) (s : ) (t : ) (s' : ) (t' : ) :
          (Nat.xgcdAux x s t y s' t').fst = Nat.gcd x y
          theorem Nat.xgcdAux_val (x : ) (y : ) :
          Nat.xgcdAux x 1 0 y 0 1 = (Nat.gcd x y, Nat.xgcd x y)
          theorem Nat.xgcd_val (x : ) (y : ) :
          Nat.xgcd x y = (Nat.gcdA x y, Nat.gcdB x 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 (Nat.xgcdAux r s t r' s' t')
          theorem Nat.gcd_eq_gcd_ab (x : ) (y : ) :
          ↑(Nat.gcd x y) = x * Nat.gcdA x y + y * Nat.gcdB x 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 : Nat.gcd n k < k) :
          m, n * m % k = Nat.gcd n k
          theorem Nat.exists_mul_emod_eq_one_of_coprime {k : } {n : } (hkn : Nat.Coprime n k) (hk : 1 < k) :
          m, n * m % k = 1

          Divisibility over ℤ #

          theorem Int.gcd_def (i : ) (j : ) :
          theorem Int.coe_nat_gcd (m : ) (n : ) :
          Int.gcd m n = Nat.gcd m n
          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 : ) :
              ↑(Int.gcd x y) = x * Int.gcdA x y + y * Int.gcdB x y

              Bézout's lemma

              theorem Int.natAbs_ediv (a : ) (b : ) (H : b a) :
              theorem Int.dvd_of_mul_dvd_mul_left {i : } {j : } {k : } (k_non_zero : k 0) (H : k * i k * j) :
              i j
              theorem Int.dvd_of_mul_dvd_mul_right {i : } {j : } {k : } (k_non_zero : k 0) (H : i * k j * k) :
              i j
              def Int.lcm (i : ) (j : ) :

              ℤ specific version of least common multiple.

              Equations
              Instances For
                theorem Int.lcm_def (i : ) (j : ) :
                theorem Int.coe_nat_lcm (m : ) (n : ) :
                Int.lcm m n = Nat.lcm m n
                theorem Int.gcd_dvd_left (i : ) (j : ) :
                ↑(Int.gcd i j) i
                theorem Int.gcd_dvd_right (i : ) (j : ) :
                ↑(Int.gcd i j) j
                theorem Int.dvd_gcd {i : } {j : } {k : } (h1 : k i) (h2 : k j) :
                k ↑(Int.gcd i j)
                theorem Int.gcd_mul_lcm (i : ) (j : ) :
                Int.gcd i j * Int.lcm i j = Int.natAbs (i * j)
                theorem Int.gcd_comm (i : ) (j : ) :
                Int.gcd i j = Int.gcd j i
                theorem Int.gcd_assoc (i : ) (j : ) (k : ) :
                Int.gcd (↑(Int.gcd i j)) k = Int.gcd i ↑(Int.gcd j k)
                @[simp]
                theorem Int.gcd_self (i : ) :
                @[simp]
                @[simp]
                @[simp]
                theorem Int.gcd_one_left (i : ) :
                Int.gcd 1 i = 1
                @[simp]
                theorem Int.gcd_one_right (i : ) :
                Int.gcd i 1 = 1
                @[simp]
                theorem Int.gcd_neg_right {x : } {y : } :
                Int.gcd x (-y) = Int.gcd x y
                @[simp]
                theorem Int.gcd_neg_left {x : } {y : } :
                Int.gcd (-x) y = Int.gcd x y
                theorem Int.gcd_mul_left (i : ) (j : ) (k : ) :
                Int.gcd (i * j) (i * k) = Int.natAbs i * Int.gcd j k
                theorem Int.gcd_mul_right (i : ) (j : ) (k : ) :
                Int.gcd (i * j) (k * j) = Int.gcd i k * Int.natAbs j
                theorem Int.gcd_pos_of_ne_zero_left {i : } (j : ) (hi : i 0) :
                0 < Int.gcd i j
                theorem Int.gcd_pos_of_ne_zero_right (i : ) {j : } (hj : j 0) :
                0 < Int.gcd i j
                theorem Int.gcd_eq_zero_iff {i : } {j : } :
                Int.gcd i j = 0 i = 0 j = 0
                theorem Int.gcd_pos_iff {i : } {j : } :
                0 < Int.gcd i j i 0 j 0
                theorem Int.gcd_div {i : } {j : } {k : } (H1 : k i) (H2 : k j) :
                Int.gcd (i / k) (j / k) = Int.gcd i j / Int.natAbs k
                theorem Int.gcd_div_gcd_div_gcd {i : } {j : } (H : 0 < Int.gcd i j) :
                Int.gcd (i / ↑(Int.gcd i j)) (j / ↑(Int.gcd i j)) = 1
                theorem Int.gcd_dvd_gcd_of_dvd_left {i : } {k : } (j : ) (H : i k) :
                theorem Int.gcd_dvd_gcd_of_dvd_right {i : } {k : } (j : ) (H : i k) :
                theorem Int.gcd_dvd_gcd_mul_left (i : ) (j : ) (k : ) :
                Int.gcd i j Int.gcd (k * i) j
                theorem Int.gcd_dvd_gcd_mul_right (i : ) (j : ) (k : ) :
                Int.gcd i j Int.gcd (i * k) j
                theorem Int.gcd_dvd_gcd_mul_left_right (i : ) (j : ) (k : ) :
                Int.gcd i j Int.gcd i (k * j)
                theorem Int.gcd_dvd_gcd_mul_right_right (i : ) (j : ) (k : ) :
                Int.gcd i j Int.gcd i (j * k)
                theorem Int.gcd_eq_left {i : } {j : } (H : i j) :
                theorem Int.gcd_eq_right {i : } {j : } (H : j i) :
                theorem Int.ne_zero_of_gcd {x : } {y : } (hc : Int.gcd x y 0) :
                x 0 y 0
                theorem Int.exists_gcd_one {m : } {n : } (H : 0 < Int.gcd m n) :
                m' n', Int.gcd m' n' = 1 m = m' * ↑(Int.gcd m n) n = n' * ↑(Int.gcd m n)
                theorem Int.exists_gcd_one' {m : } {n : } (H : 0 < Int.gcd m n) :
                g m' n', 0 < g Int.gcd m' n' = 1 m = m' * g n = n' * g
                theorem Int.pow_dvd_pow_iff {m : } {n : } {k : } (k0 : 0 < k) :
                m ^ k n ^ k m n
                theorem Int.gcd_dvd_iff {a : } {b : } {n : } :
                Int.gcd a 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 = ↑(Int.gcd a b)
                theorem Int.dvd_of_dvd_mul_left_of_gcd_one {a : } {b : } {c : } (habc : a b * c) (hab : Int.gcd a 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 : Int.gcd a 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} (Int.gcd a 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 : ) :
                Int.lcm i j = Int.lcm j i
                theorem Int.lcm_assoc (i : ) (j : ) (k : ) :
                Int.lcm (↑(Int.lcm i j)) k = Int.lcm i ↑(Int.lcm j k)
                @[simp]
                theorem Int.lcm_zero_left (i : ) :
                Int.lcm 0 i = 0
                @[simp]
                theorem Int.lcm_zero_right (i : ) :
                Int.lcm i 0 = 0
                @[simp]
                theorem Int.lcm_one_left (i : ) :
                @[simp]
                @[simp]
                theorem Int.lcm_self (i : ) :
                theorem Int.dvd_lcm_left (i : ) (j : ) :
                i ↑(Int.lcm i j)
                theorem Int.dvd_lcm_right (i : ) (j : ) :
                j ↑(Int.lcm i j)
                theorem Int.lcm_dvd {i : } {j : } {k : } :
                i kj k↑(Int.lcm i j) k
                theorem Int.lcm_mul_left {m : } {n : } {k : } :
                Int.lcm (m * n) (m * k) = Int.natAbs m * Int.lcm n k
                theorem Int.lcm_mul_right {m : } {n : } {k : } :
                Int.lcm (m * n) (k * n) = Int.lcm m k * Int.natAbs n
                theorem gcd_nsmul_eq_zero {M : Type u_1} [AddMonoid M] (x : M) {m : } {n : } (hm : m x = 0) (hn : n x = 0) :
                Nat.gcd m 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 ^ Nat.gcd m n = 1