Documentation

Std.Data.Nat.Gcd

Definitions and properties of gcd, lcm, and coprime #

theorem Nat.gcd_rec (m : Nat) (n : Nat) :
Nat.gcd m n = Nat.gcd (n % m) m
theorem Nat.gcd.induction {P : NatNatProp} (m : Nat) (n : Nat) (H0 : (n : Nat) → P 0 n) (H1 : (m n : Nat) → 0 < mP (n % m) mP m n) :
P m n
def Nat.lcm (m : Nat) (n : Nat) :

The least common multiple of m and n, defined using gcd.

Equations
Instances For
    @[reducible]
    def Nat.Coprime (m : Nat) (n : Nat) :

    m and n are coprime, or relatively prime, if their gcd is 1.

    Equations
    Instances For
      theorem Nat.gcd_dvd (m : Nat) (n : Nat) :
      Nat.gcd m n m Nat.gcd m n n
      theorem Nat.gcd_dvd_left (m : Nat) (n : Nat) :
      Nat.gcd m n m
      theorem Nat.gcd_dvd_right (m : Nat) (n : Nat) :
      Nat.gcd m n n
      theorem Nat.gcd_le_left {m : Nat} (n : Nat) (h : 0 < m) :
      Nat.gcd m n m
      theorem Nat.gcd_le_right {m : Nat} (n : Nat) (h : 0 < n) :
      Nat.gcd m n n
      theorem Nat.dvd_gcd {k : Nat} {m : Nat} {n : Nat} :
      k mk nk Nat.gcd m n
      theorem Nat.dvd_gcd_iff {k : Nat} {m : Nat} {n : Nat} :
      k Nat.gcd m n k m k n
      theorem Nat.gcd_comm (m : Nat) (n : Nat) :
      Nat.gcd m n = Nat.gcd n m
      theorem Nat.gcd_eq_left_iff_dvd {m : Nat} {n : Nat} :
      m n Nat.gcd m n = m
      theorem Nat.gcd_eq_right_iff_dvd {m : Nat} {n : Nat} :
      m n Nat.gcd n m = m
      theorem Nat.gcd_assoc (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd (Nat.gcd m n) k = Nat.gcd m (Nat.gcd n k)
      @[simp]
      theorem Nat.gcd_one_right (n : Nat) :
      Nat.gcd n 1 = 1
      theorem Nat.gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd (m * n) (m * k) = m * Nat.gcd n k
      theorem Nat.gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd (m * n) (k * n) = Nat.gcd m k * n
      theorem Nat.gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) :
      0 < Nat.gcd m n
      theorem Nat.gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) :
      0 < Nat.gcd m n
      theorem Nat.div_gcd_pos_of_pos_left {a : Nat} (b : Nat) (h : 0 < a) :
      0 < a / Nat.gcd a b
      theorem Nat.div_gcd_pos_of_pos_right {b : Nat} (a : Nat) (h : 0 < b) :
      0 < b / Nat.gcd a b
      theorem Nat.eq_zero_of_gcd_eq_zero_left {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
      m = 0
      theorem Nat.eq_zero_of_gcd_eq_zero_right {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
      n = 0
      theorem Nat.gcd_ne_zero_left {m : Nat} {n : Nat} :
      m 0Nat.gcd m n 0
      theorem Nat.gcd_ne_zero_right {n : Nat} {m : Nat} :
      n 0Nat.gcd m n 0
      theorem Nat.gcd_div {m : Nat} {n : Nat} {k : Nat} (H1 : k m) (H2 : k n) :
      Nat.gcd (m / k) (n / k) = Nat.gcd m n / k
      theorem Nat.gcd_dvd_gcd_of_dvd_left {m : Nat} {k : Nat} (n : Nat) (H : m k) :
      theorem Nat.gcd_dvd_gcd_of_dvd_right {m : Nat} {k : Nat} (n : Nat) (H : m k) :
      theorem Nat.gcd_dvd_gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd m n Nat.gcd (k * m) n
      theorem Nat.gcd_dvd_gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd m n Nat.gcd (m * k) n
      theorem Nat.gcd_dvd_gcd_mul_left_right (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd m n Nat.gcd m (k * n)
      theorem Nat.gcd_dvd_gcd_mul_right_right (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd m n Nat.gcd m (n * k)
      theorem Nat.gcd_eq_left {m : Nat} {n : Nat} (H : m n) :
      Nat.gcd m n = m
      theorem Nat.gcd_eq_right {m : Nat} {n : Nat} (H : n m) :
      Nat.gcd m n = n
      @[simp]
      theorem Nat.gcd_mul_left_left (m : Nat) (n : Nat) :
      Nat.gcd (m * n) n = n
      @[simp]
      theorem Nat.gcd_mul_left_right (m : Nat) (n : Nat) :
      Nat.gcd n (m * n) = n
      @[simp]
      theorem Nat.gcd_mul_right_left (m : Nat) (n : Nat) :
      Nat.gcd (n * m) n = n
      @[simp]
      theorem Nat.gcd_mul_right_right (m : Nat) (n : Nat) :
      Nat.gcd n (n * m) = n
      @[simp]
      theorem Nat.gcd_gcd_self_right_left (m : Nat) (n : Nat) :
      Nat.gcd m (Nat.gcd m n) = Nat.gcd m n
      @[simp]
      theorem Nat.gcd_gcd_self_right_right (m : Nat) (n : Nat) :
      Nat.gcd m (Nat.gcd n m) = Nat.gcd n m
      @[simp]
      theorem Nat.gcd_gcd_self_left_right (m : Nat) (n : Nat) :
      Nat.gcd (Nat.gcd n m) m = Nat.gcd n m
      @[simp]
      theorem Nat.gcd_gcd_self_left_left (m : Nat) (n : Nat) :
      Nat.gcd (Nat.gcd m n) m = Nat.gcd m n
      theorem Nat.gcd_add_mul_self (m : Nat) (n : Nat) (k : Nat) :
      Nat.gcd m (n + k * m) = Nat.gcd m n
      theorem Nat.gcd_eq_zero_iff {i : Nat} {j : Nat} :
      Nat.gcd i j = 0 i = 0 j = 0

      lcm #

      theorem Nat.lcm_comm (m : Nat) (n : Nat) :
      Nat.lcm m n = Nat.lcm n m
      @[simp]
      theorem Nat.lcm_zero_left (m : Nat) :
      Nat.lcm 0 m = 0
      @[simp]
      theorem Nat.lcm_zero_right (m : Nat) :
      Nat.lcm m 0 = 0
      @[simp]
      theorem Nat.lcm_one_left (m : Nat) :
      Nat.lcm 1 m = m
      @[simp]
      theorem Nat.lcm_one_right (m : Nat) :
      Nat.lcm m 1 = m
      @[simp]
      theorem Nat.lcm_self (m : Nat) :
      Nat.lcm m m = m
      theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) :
      m Nat.lcm m n
      theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) :
      n Nat.lcm m n
      theorem Nat.gcd_mul_lcm (m : Nat) (n : Nat) :
      Nat.gcd m n * Nat.lcm m n = m * n
      theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m k) (H2 : n k) :
      Nat.lcm m n k
      theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) :
      Nat.lcm (Nat.lcm m n) k = Nat.lcm m (Nat.lcm n k)
      theorem Nat.lcm_ne_zero {m : Nat} {n : Nat} (hm : m 0) (hn : n 0) :
      Nat.lcm m n 0

      coprime #

      See also nat.coprime_of_dvd and nat.coprime_of_dvd' to prove nat.Coprime m n.

      theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} :
      Nat.Coprime m nNat.gcd m n = 1
      theorem Nat.Coprime.symm {n : Nat} {m : Nat} :
      theorem Nat.Coprime.dvd_of_dvd_mul_right {k : Nat} {n : Nat} {m : Nat} (H1 : Nat.Coprime k n) (H2 : k m * n) :
      k m
      theorem Nat.Coprime.dvd_of_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (H1 : Nat.Coprime k m) (H2 : k m * n) :
      k n
      theorem Nat.Coprime.gcd_mul_left_cancel {k : Nat} {n : Nat} (m : Nat) (H : Nat.Coprime k n) :
      Nat.gcd (k * m) n = Nat.gcd m n
      theorem Nat.Coprime.gcd_mul_right_cancel {k : Nat} {n : Nat} (m : Nat) (H : Nat.Coprime k n) :
      Nat.gcd (m * k) n = Nat.gcd m n
      theorem Nat.Coprime.gcd_mul_left_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : Nat.Coprime k m) :
      Nat.gcd m (k * n) = Nat.gcd m n
      theorem Nat.Coprime.gcd_mul_right_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : Nat.Coprime k m) :
      Nat.gcd m (n * k) = Nat.gcd m n
      theorem Nat.coprime_div_gcd_div_gcd {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
      Nat.Coprime (m / Nat.gcd m n) (n / Nat.gcd m n)
      theorem Nat.not_coprime_of_dvd_of_dvd {d : Nat} {m : Nat} {n : Nat} (dgt1 : 1 < d) (Hm : d m) (Hn : d n) :
      theorem Nat.exists_coprime {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
      m' n', Nat.Coprime m' n' m = m' * Nat.gcd m n n = n' * Nat.gcd m n
      theorem Nat.exists_coprime' {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
      g m' n', 0 < g Nat.Coprime m' n' m = m' * g n = n' * g
      theorem Nat.Coprime.mul {m : Nat} {k : Nat} {n : Nat} (H1 : Nat.Coprime m k) (H2 : Nat.Coprime n k) :
      Nat.Coprime (m * n) k
      theorem Nat.Coprime.mul_right {k : Nat} {m : Nat} {n : Nat} (H1 : Nat.Coprime k m) (H2 : Nat.Coprime k n) :
      Nat.Coprime k (m * n)
      theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m k) (H2 : Nat.Coprime k n) :
      theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n m) (H2 : Nat.Coprime k m) :
      theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : Nat.Coprime (k * m) n) :
      theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime (m * k) n) :
      theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime m (k * n)) :
      theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : Nat.Coprime m (n * k)) :
      theorem Nat.Coprime.coprime_div_left {m : Nat} {n : Nat} {a : Nat} (cmn : Nat.Coprime m n) (dvd : a m) :
      Nat.Coprime (m / a) n
      theorem Nat.Coprime.coprime_div_right {m : Nat} {n : Nat} {a : Nat} (cmn : Nat.Coprime m n) (dvd : a n) :
      Nat.Coprime m (n / a)
      theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) :
      theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) :
      theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : Nat.Coprime m n) :
      theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd {m : Nat} {n : Nat} {a : Nat} (hmn : Nat.Coprime m n) (hm : m a) (hn : n a) :
      m * n a
      @[simp]
      theorem Nat.coprime_zero_left (n : Nat) :
      Nat.Coprime 0 n n = 1
      @[simp]
      theorem Nat.coprime_zero_right (n : Nat) :
      Nat.Coprime n 0 n = 1
      @[simp]
      theorem Nat.coprime_self (n : Nat) :
      Nat.Coprime n n n = 1
      theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : Nat.Coprime m k) :
      Nat.Coprime (m ^ n) k
      theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : Nat.Coprime k m) :
      Nat.Coprime k (m ^ n)
      theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : Nat.Coprime k l) :
      Nat.Coprime (k ^ m) (l ^ n)
      theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : Nat.Coprime k m) (d : k m) :
      k = 1
      def Nat.prod_dvd_and_dvd_of_dvd_prod {k : Nat} {m : Nat} {n : Nat} (H : k m * n) :
      { d // k = d.fst.val * d.snd.val }

      Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Nat.gcd_mul_dvd_mul_gcd (k : Nat) (m : Nat) (n : Nat) :
        Nat.gcd k (m * n) Nat.gcd k m * Nat.gcd k n
        theorem Nat.Coprime.gcd_mul {m : Nat} {n : Nat} (k : Nat) (h : Nat.Coprime m n) :
        Nat.gcd k (m * n) = Nat.gcd k m * Nat.gcd k n
        theorem Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {c : Nat} {d : Nat} {a : Nat} {b : Nat} (cop : Nat.Coprime c d) (h : a * b = c * d) :
        Nat.gcd a c * Nat.gcd b c = c