HepLean Documentation

Batteries.Data.Nat.Gcd

Definitions and properties of coprime #

coprime #

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

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

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

Equations
  • m.Coprime n = (m.gcd n = 1)
Instances For
    source
    instance Nat.instDecidableCoprime (m : Nat) (n : Nat) :
    Decidable (m.Coprime n)
    Equations
    source
    theorem Nat.coprime_iff_gcd_eq_one {m : Nat} {n : Nat} :
    m.Coprime n ↔ m.gcd n = 1
    source
    theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} :
    m.Coprime n → m.gcd n = 1
    source
    theorem Nat.Coprime.symm {n : Nat} {m : Nat} :
    n.Coprime m → m.Coprime n
    source
    theorem Nat.coprime_comm {n : Nat} {m : Nat} :
    n.Coprime m ↔ m.Coprime n
    source
    theorem Nat.Coprime.dvd_of_dvd_mul_right {k : Nat} {n : Nat} {m : Nat} (H1 : k.Coprime n) (H2 : k ∣ m * n) :
    k ∣ m
    source
    theorem Nat.Coprime.dvd_of_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (H1 : k.Coprime m) (H2 : k ∣ m * n) :
    k ∣ n
    source
    theorem Nat.Coprime.gcd_mul_left_cancel {k : Nat} {n : Nat} (m : Nat) (H : k.Coprime n) :
    (k * m).gcd n = m.gcd n
    source
    theorem Nat.Coprime.gcd_mul_right_cancel {k : Nat} {n : Nat} (m : Nat) (H : k.Coprime n) :
    (m * k).gcd n = m.gcd n
    source
    theorem Nat.Coprime.gcd_mul_left_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : k.Coprime m) :
    m.gcd (k * n) = m.gcd n
    source
    theorem Nat.Coprime.gcd_mul_right_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : k.Coprime m) :
    m.gcd (n * k) = m.gcd n
    source
    theorem Nat.coprime_div_gcd_div_gcd {m : Nat} {n : Nat} (H : 0 < m.gcd n) :
    (m / m.gcd n).Coprime (n / m.gcd 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) :
    ¬m.Coprime n
    source
    theorem Nat.exists_coprime (m : Nat) (n : Nat) :
    ∃ (m' : Nat), ∃ (n' : Nat), m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n
    source
    theorem Nat.exists_coprime' {m : Nat} {n : Nat} (H : 0 < m.gcd n) :
    ∃ (g : Nat), ∃ (m' : Nat), ∃ (n' : Nat), 0 < g ∧ m'.Coprime n' ∧ m = m' * g ∧ n = n' * g
    source
    theorem Nat.Coprime.mul {m : Nat} {k : Nat} {n : Nat} (H1 : m.Coprime k) (H2 : n.Coprime k) :
    (m * n).Coprime k
    source
    theorem Nat.Coprime.mul_right {k : Nat} {m : Nat} {n : Nat} (H1 : k.Coprime m) (H2 : k.Coprime n) :
    k.Coprime (m * n)
    source
    theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m ∣ k) (H2 : k.Coprime n) :
    m.Coprime n
    source
    theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n ∣ m) (H2 : k.Coprime m) :
    k.Coprime n
    source
    theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : (k * m).Coprime n) :
    m.Coprime n
    source
    theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : (m * k).Coprime n) :
    m.Coprime n
    source
    theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : m.Coprime (k * n)) :
    m.Coprime n
    source
    theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : m.Coprime (n * k)) :
    m.Coprime n
    source
    theorem Nat.Coprime.coprime_div_left {m : Nat} {n : Nat} {a : Nat} (cmn : m.Coprime n) (dvd : a ∣ m) :
    (m / a).Coprime n
    source
    theorem Nat.Coprime.coprime_div_right {m : Nat} {n : Nat} {a : Nat} (cmn : m.Coprime n) (dvd : a ∣ n) :
    m.Coprime (n / a)
    source
    theorem Nat.coprime_mul_iff_left {m : Nat} {n : Nat} {k : Nat} :
    (m * n).Coprime k ↔ m.Coprime k ∧ n.Coprime k
    source
    theorem Nat.coprime_mul_iff_right {k : Nat} {m : Nat} {n : Nat} :
    k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime n
    source
    theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : m.Coprime n) :
    (k.gcd m).Coprime n
    source
    theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : m.Coprime n) :
    m.Coprime (k.gcd n)
    source
    theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : m.Coprime n) :
    (k.gcd m).Coprime (l.gcd n)
    source
    theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd {m : Nat} {n : Nat} {a : Nat} (hmn : m.Coprime 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) :
    n.Coprime 0 ↔ n = 1
    source
    theorem Nat.coprime_one_left (n : Nat) :
    Nat.Coprime 1 n
    source
    theorem Nat.coprime_one_right (n : Nat) :
    n.Coprime 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) :
    n.Coprime 1 = True
    source
    @[simp]
    theorem Nat.coprime_self (n : Nat) :
    n.Coprime n ↔ n = 1
    source
    theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : m.Coprime k) :
    (m ^ n).Coprime k
    source
    theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : k.Coprime m) :
    k.Coprime (m ^ n)
    source
    theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : k.Coprime l) :
    (k ^ m).Coprime (l ^ n)
    source
    theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : k.Coprime m) (d : k ∣ m) :
    k = 1
    source
    theorem Nat.Coprime.gcd_mul {m : Nat} {n : Nat} (k : Nat) (h : m.Coprime n) :
    k.gcd (m * n) = k.gcd m * k.gcd n
    source
    theorem Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {c : Nat} {d : Nat} {a : Nat} {b : Nat} (cop : c.Coprime d) (h : a * b = c * d) :
    a.gcd c * b.gcd c = c