Documentation

Std.Data.Nat.Gcd

Definitions and properties of gcd, lcm, and coprime #

source
@[reducible]
def Nat.Coprime (m : Nat) (n : Nat) :
Prop

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

Equations
Instances For
    source
    theorem Nat.dvd_gcd_iff {k : Nat} {m : Nat} {n : Nat} :
    k ∣ Nat.gcd m n ↔ k ∣ m ∧ k ∣ n
    source
    theorem Nat.gcd_comm (m : Nat) (n : Nat) :
    Nat.gcd m n = Nat.gcd n m
    source
    theorem Nat.gcd_eq_left_iff_dvd {m : Nat} {n : Nat} :
    m ∣ n ↔ Nat.gcd m n = m
    source
    theorem Nat.gcd_eq_right_iff_dvd {m : Nat} {n : Nat} :
    m ∣ n ↔ Nat.gcd n m = m
    source
    theorem Nat.gcd_assoc (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd (Nat.gcd m n) k = Nat.gcd m (Nat.gcd n k)
    source
    @[simp]
    theorem Nat.gcd_one_right (n : Nat) :
    Nat.gcd n 1 = 1
    source
    theorem Nat.gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd (m * n) (m * k) = m * Nat.gcd n k
    source
    theorem Nat.gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd (m * n) (k * n) = Nat.gcd m k * n
    source
    theorem Nat.gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) :
    0 < Nat.gcd m n
    source
    theorem Nat.gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) :
    0 < Nat.gcd m n
    source
    theorem Nat.div_gcd_pos_of_pos_left {a : Nat} (b : Nat) (h : 0 < a) :
    0 < a / Nat.gcd a b
    source
    theorem Nat.div_gcd_pos_of_pos_right {b : Nat} (a : Nat) (h : 0 < b) :
    0 < b / Nat.gcd a b
    source
    theorem Nat.eq_zero_of_gcd_eq_zero_left {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
    m = 0
    source
    theorem Nat.eq_zero_of_gcd_eq_zero_right {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) :
    n = 0
    source
    theorem Nat.gcd_ne_zero_left {m : Nat} {n : Nat} :
    m ≠ 0 → Nat.gcd m n ≠ 0
    source
    theorem Nat.gcd_ne_zero_right {n : Nat} {m : Nat} :
    n ≠ 0 → Nat.gcd m n ≠ 0
    source
    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
    source
    theorem Nat.gcd_dvd_gcd_of_dvd_left {m : Nat} {k : Nat} (n : Nat) (H : m ∣ k) :
    Nat.gcd m n ∣ Nat.gcd k n
    source
    theorem Nat.gcd_dvd_gcd_of_dvd_right {m : Nat} {k : Nat} (n : Nat) (H : m ∣ k) :
    Nat.gcd n m ∣ Nat.gcd n k
    source
    theorem Nat.gcd_dvd_gcd_mul_left (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd m n ∣ Nat.gcd (k * m) n
    source
    theorem Nat.gcd_dvd_gcd_mul_right (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd m n ∣ Nat.gcd (m * k) n
    source
    theorem Nat.gcd_dvd_gcd_mul_left_right (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd m n ∣ Nat.gcd m (k * n)
    source
    theorem Nat.gcd_dvd_gcd_mul_right_right (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd m n ∣ Nat.gcd m (n * k)
    source
    theorem Nat.gcd_eq_left {m : Nat} {n : Nat} (H : m ∣ n) :
    Nat.gcd m n = m
    source
    theorem Nat.gcd_eq_right {m : Nat} {n : Nat} (H : n ∣ m) :
    Nat.gcd m n = n
    source
    @[simp]
    theorem Nat.gcd_mul_left_left (m : Nat) (n : Nat) :
    Nat.gcd (m * n) n = n
    source
    @[simp]
    theorem Nat.gcd_mul_left_right (m : Nat) (n : Nat) :
    Nat.gcd n (m * n) = n
    source
    @[simp]
    theorem Nat.gcd_mul_right_left (m : Nat) (n : Nat) :
    Nat.gcd (n * m) n = n
    source
    @[simp]
    theorem Nat.gcd_mul_right_right (m : Nat) (n : Nat) :
    Nat.gcd n (n * m) = n
    source
    @[simp]
    theorem Nat.gcd_gcd_self_right_left (m : Nat) (n : Nat) :
    Nat.gcd m (Nat.gcd m n) = Nat.gcd m n
    source
    @[simp]
    theorem Nat.gcd_gcd_self_right_right (m : Nat) (n : Nat) :
    Nat.gcd m (Nat.gcd n m) = Nat.gcd n m
    source
    @[simp]
    theorem Nat.gcd_gcd_self_left_right (m : Nat) (n : Nat) :
    Nat.gcd (Nat.gcd n m) m = Nat.gcd n m
    source
    @[simp]
    theorem Nat.gcd_gcd_self_left_left (m : Nat) (n : Nat) :
    Nat.gcd (Nat.gcd m n) m = Nat.gcd m n
    source
    theorem Nat.gcd_add_mul_self (m : Nat) (n : Nat) (k : Nat) :
    Nat.gcd m (n + k * m) = Nat.gcd m n
    source
    theorem Nat.gcd_eq_zero_iff {i : Nat} {j : Nat} :
    Nat.gcd i j = 0 ↔ i = 0 ∧ j = 0
    source
    theorem Nat.gcd_eq_iff {g : Nat} (a : Nat) (b : Nat) :
    Nat.gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g

    Characterization of the value of Nat.gcd.

    lcm #

    source
    theorem Nat.lcm_comm (m : Nat) (n : Nat) :
    Nat.lcm m n = Nat.lcm n m
    source
    @[simp]
    theorem Nat.lcm_zero_left (m : Nat) :
    Nat.lcm 0 m = 0
    source
    @[simp]
    theorem Nat.lcm_zero_right (m : Nat) :
    Nat.lcm m 0 = 0
    source
    @[simp]
    theorem Nat.lcm_one_left (m : Nat) :
    Nat.lcm 1 m = m
    source
    @[simp]
    theorem Nat.lcm_one_right (m : Nat) :
    Nat.lcm m 1 = m
    source
    @[simp]
    theorem Nat.lcm_self (m : Nat) :
    Nat.lcm m m = m
    source
    theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) :
    m ∣ Nat.lcm m n
    source
    theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) :
    n ∣ Nat.lcm m n
    source
    theorem Nat.gcd_mul_lcm (m : Nat) (n : Nat) :
    Nat.gcd m n * Nat.lcm m n = m * n
    source
    theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) :
    Nat.lcm m n ∣ k
    source
    theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) :
    Nat.lcm (Nat.lcm m n) k = Nat.lcm m (Nat.lcm n k)
    source
    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.

    source
    instance Nat.instDecidableCoprime (m : Nat) (n : Nat) :
    Decidable (Nat.Coprime m n)
    Equations
    source
    theorem Nat.coprime_iff_gcd_eq_one {m : Nat} {n : Nat} :
    Nat.Coprime m n ↔ Nat.gcd m n = 1
    source
    theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} :
    Nat.Coprime m n → Nat.gcd m n = 1
    source
    theorem Nat.Coprime.symm {n : Nat} {m : Nat} :
    Nat.Coprime n m → Nat.Coprime m n
    source
    theorem Nat.coprime_comm {n : Nat} {m : Nat} :
    Nat.Coprime n m ↔ Nat.Coprime m n
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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)
    source
    theorem Nat.not_coprime_of_dvd_of_dvd {d : Nat} {m : Nat} {n : Nat} (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) :
    ¬Nat.Coprime m n
    source
    theorem Nat.exists_coprime {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
    ∃ (m' : Nat), ∃ (n' : Nat), Nat.Coprime m' n' ∧ m = m' * Nat.gcd m n ∧ n = n' * Nat.gcd m n
    source
    theorem Nat.exists_coprime' {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) :
    ∃ (g : Nat), ∃ (m' : Nat), ∃ (n' : Nat), 0 < g ∧ Nat.Coprime m' n' ∧ m = m' * g ∧ n = n' * g
    source
    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
    source
    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)
    source
    theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m ∣ k) (H2 : Nat.Coprime k n) :
    Nat.Coprime m n
    source
    theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n ∣ m) (H2 : Nat.Coprime k m) :
    Nat.Coprime k n
    source
    theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : Nat.Coprime (k * m) n) :
    Nat.Coprime m n
    source
    theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime (m * k) n) :
    Nat.Coprime m n
    source
    theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime m (k * n)) :
    Nat.Coprime m n
    source
    theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : Nat.Coprime m (n * k)) :
    Nat.Coprime m n
    source
    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
    source
    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)
    source
    theorem Nat.coprime_mul_iff_left {m : Nat} {n : Nat} {k : Nat} :
    Nat.Coprime (m * n) k ↔ Nat.Coprime m k ∧ Nat.Coprime n k
    source
    theorem Nat.coprime_mul_iff_right {k : Nat} {m : Nat} {n : Nat} :
    Nat.Coprime k (m * n) ↔ Nat.Coprime k m ∧ Nat.Coprime k n
    source
    theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) :
    Nat.Coprime (Nat.gcd k m) n
    source
    theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) :
    Nat.Coprime m (Nat.gcd k n)
    source
    theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : Nat.Coprime m n) :
    Nat.Coprime (Nat.gcd k m) (Nat.gcd l n)
    source
    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
    source
    @[simp]
    theorem Nat.coprime_zero_left (n : Nat) :
    Nat.Coprime 0 n ↔ n = 1
    source
    @[simp]
    theorem Nat.coprime_zero_right (n : Nat) :
    Nat.Coprime n 0 ↔ n = 1
    source
    theorem Nat.coprime_one_left (n : Nat) :
    Nat.Coprime 1 n
    source
    theorem Nat.coprime_one_right (n : Nat) :
    Nat.Coprime n 1
    source
    @[simp]
    theorem Nat.coprime_one_left_eq_true (n : Nat) :
    Nat.Coprime 1 n = True
    source
    @[simp]
    theorem Nat.coprime_one_right_eq_true (n : Nat) :
    Nat.Coprime n 1 = True
    source
    @[simp]
    theorem Nat.coprime_self (n : Nat) :
    Nat.Coprime n n ↔ n = 1
    source
    theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : Nat.Coprime m k) :
    Nat.Coprime (m ^ n) k
    source
    theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : Nat.Coprime k m) :
    Nat.Coprime k (m ^ n)
    source
    theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : Nat.Coprime k l) :
    Nat.Coprime (k ^ m) (l ^ n)
    source
    theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : Nat.Coprime k m) (d : k ∣ m) :
    k = 1
    source
    def Nat.prod_dvd_and_dvd_of_dvd_prod {k : Nat} {m : Nat} {n : Nat} (H : k ∣ m * n) :
    { d : { m' : Nat // m' ∣ m } × { n' : Nat // n' ∣ n } // 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
      source
      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
      source
      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
      source
      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