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.

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

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

Equations
Instances For
    theorem Nat.Coprime.gcd_eq_one {m n : Nat} :
    m.Coprime nm.gcd n = 1
    theorem Nat.Coprime.symm {n m : Nat} :
    n.Coprime mm.Coprime n
    theorem Nat.Coprime.dvd_of_dvd_mul_right {k n m : Nat} (H1 : k.Coprime n) (H2 : k m * n) :
    theorem Nat.Coprime.dvd_of_dvd_mul_left {k m n : Nat} (H1 : k.Coprime m) (H2 : k m * n) :
    theorem Nat.Coprime.gcd_mul_left_cancel {k n : Nat} (m : Nat) (H : k.Coprime n) :
    (k * m).gcd n = m.gcd n
    theorem Nat.Coprime.gcd_mul_right_cancel {k n : Nat} (m : Nat) (H : k.Coprime n) :
    (m * k).gcd n = m.gcd n
    theorem Nat.Coprime.gcd_mul_left_cancel_right {k m : Nat} (n : Nat) (H : k.Coprime m) :
    m.gcd (k * n) = m.gcd n
    theorem Nat.Coprime.gcd_mul_right_cancel_right {k m : Nat} (n : Nat) (H : k.Coprime m) :
    m.gcd (n * k) = m.gcd n
    theorem Nat.coprime_div_gcd_div_gcd {m 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 m n : Nat} (dgt1 : 1 < d) (Hm : d m) (Hn : d n) :
    theorem Nat.Coprime.mul {m k n : Nat} (H1 : m.Coprime k) (H2 : n.Coprime k) :
    theorem Nat.Coprime.mul_right {k m n : Nat} (H1 : k.Coprime m) (H2 : k.Coprime n) :
    theorem Nat.Coprime.coprime_dvd_left {m k n : Nat} (H1 : m k) (H2 : k.Coprime n) :
    theorem Nat.Coprime.coprime_dvd_right {n m k : Nat} (H1 : n m) (H2 : k.Coprime m) :
    theorem Nat.Coprime.coprime_mul_left {k m n : Nat} (H : (k * m).Coprime n) :
    theorem Nat.Coprime.coprime_mul_right {m k n : Nat} (H : (m * k).Coprime n) :
    theorem Nat.Coprime.coprime_div_left {m n a : Nat} (cmn : m.Coprime n) (dvd : a m) :
    theorem Nat.Coprime.coprime_div_right {m n a : Nat} (cmn : m.Coprime n) (dvd : a n) :
    theorem Nat.Coprime.gcd_left {m n : Nat} (k : Nat) (hmn : m.Coprime n) :
    (k.gcd m).Coprime n
    theorem Nat.Coprime.gcd_right {m n : Nat} (k : Nat) (hmn : m.Coprime n) :
    m.Coprime (k.gcd n)
    theorem Nat.Coprime.gcd_both {m n : Nat} (k l : Nat) (hmn : m.Coprime n) :
    (k.gcd m).Coprime (l.gcd n)
    theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd {m n a : Nat} (hmn : m.Coprime n) (hm : m a) (hn : n a) :
    m * n a
    @[simp]
    theorem Nat.coprime_zero_left (n : Nat) :
    @[simp]
    @[simp]
    theorem Nat.coprime_self (n : Nat) :
    theorem Nat.Coprime.pow_left {m k : Nat} (n : Nat) (H1 : m.Coprime k) :
    theorem Nat.Coprime.pow_right {k m : Nat} (n : Nat) (H1 : k.Coprime m) :
    theorem Nat.Coprime.pow {k l : Nat} (m n : Nat) (H1 : k.Coprime l) :
    theorem Nat.Coprime.eq_one_of_dvd {k m : Nat} (H : k.Coprime m) (d : k m) :
    k = 1
    theorem Nat.Coprime.gcd_mul {m 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 d a b : Nat} (cop : c.Coprime d) (h : a * b = c * d) :
    a.gcd c * b.gcd c = c