# Definitions and properties of coprime#

### coprime#

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

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

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

Equations
• m.Coprime n = (m.gcd n = 1)
Instances For
instance Nat.instDecidableCoprime (m : Nat) (n : Nat) :
Decidable (m.Coprime n)
Equations
theorem Nat.coprime_iff_gcd_eq_one {m : Nat} {n : Nat} :
m.Coprime n m.gcd n = 1
theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} :
m.Coprime nm.gcd n = 1
theorem Nat.Coprime.symm {n : Nat} {m : Nat} :
n.Coprime mm.Coprime n
theorem Nat.coprime_comm {n : Nat} {m : Nat} :
n.Coprime m m.Coprime n
theorem Nat.Coprime.dvd_of_dvd_mul_right {k : Nat} {n : Nat} {m : Nat} (H1 : k.Coprime n) (H2 : k m * n) :
k m
theorem Nat.Coprime.dvd_of_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (H1 : k.Coprime m) (H2 : k m * n) :
k n
theorem Nat.Coprime.gcd_mul_left_cancel {k : Nat} {n : Nat} (m : Nat) (H : k.Coprime n) :
(k * m).gcd n = m.gcd n
theorem Nat.Coprime.gcd_mul_right_cancel {k : Nat} {n : Nat} (m : Nat) (H : k.Coprime n) :
(m * k).gcd n = m.gcd n
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
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
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)
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
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
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
theorem Nat.Coprime.mul {m : Nat} {k : Nat} {n : Nat} (H1 : m.Coprime k) (H2 : n.Coprime k) :
(m * n).Coprime k
theorem Nat.Coprime.mul_right {k : Nat} {m : Nat} {n : Nat} (H1 : k.Coprime m) (H2 : k.Coprime n) :
k.Coprime (m * n)
theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m k) (H2 : k.Coprime n) :
m.Coprime n
theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n m) (H2 : k.Coprime m) :
k.Coprime n
theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : (k * m).Coprime n) :
m.Coprime n
theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : (m * k).Coprime n) :
m.Coprime n
theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : m.Coprime (k * n)) :
m.Coprime n
theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : m.Coprime (n * k)) :
m.Coprime n
theorem Nat.Coprime.coprime_div_left {m : Nat} {n : Nat} {a : Nat} (cmn : m.Coprime n) (dvd : a m) :
(m / a).Coprime n
theorem Nat.Coprime.coprime_div_right {m : Nat} {n : Nat} {a : Nat} (cmn : m.Coprime n) (dvd : a n) :
m.Coprime (n / a)
theorem Nat.coprime_mul_iff_left {m : Nat} {n : Nat} {k : Nat} :
(m * n).Coprime k m.Coprime k n.Coprime k
theorem Nat.coprime_mul_iff_right {k : Nat} {m : Nat} {n : Nat} :
k.Coprime (m * n) k.Coprime m k.Coprime n
theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : m.Coprime n) :
(k.gcd m).Coprime n
theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : m.Coprime n) :
m.Coprime (k.gcd n)
theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : m.Coprime n) :
(k.gcd m).Coprime (l.gcd n)
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
@[simp]
theorem Nat.coprime_zero_left (n : Nat) :
n = 1
@[simp]
theorem Nat.coprime_zero_right (n : Nat) :
n.Coprime 0 n = 1
theorem Nat.coprime_one_right (n : Nat) :
n.Coprime 1
@[simp]
theorem Nat.coprime_one_right_eq_true (n : Nat) :
n.Coprime 1 = True
@[simp]
theorem Nat.coprime_self (n : Nat) :
n.Coprime n n = 1
theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : m.Coprime k) :
(m ^ n).Coprime k
theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : k.Coprime m) :
k.Coprime (m ^ n)
theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : k.Coprime l) :
(k ^ m).Coprime (l ^ n)
theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : k.Coprime m) (d : k m) :
k = 1
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
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