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

m.Coprime n = (m.gcd n = 1)

Instances For

@[inline]

instance Nat.instDecidableCoprime (m n : Nat) :

Decidable (m.Coprime n)

Equations

m.instDecidableCoprime n = inferInstanceAs (Decidable (m.gcd n = 1))

theorem Nat.coprime_iff_gcd_eq_one {m n : Nat} :

m.Coprime n ↔ m.gcd n = 1

theorem Nat.Coprime.gcd_eq_one {m n : Nat} :

m.Coprime n → m.gcd n = 1

theorem Nat.Coprime.symm {n m : Nat} :

n.Coprime m → m.Coprime n

theorem Nat.coprime_comm {n m : Nat} :

n.Coprime m ↔ m.Coprime n

theorem Nat.Coprime.dvd_of_dvd_mul_right {k n m : Nat} (H1 : k.Coprime n) (H2 : k ∣ m * n) :

k ∣ m

theorem Nat.Coprime.dvd_of_dvd_mul_left {k m n : Nat} (H1 : k.Coprime m) (H2 : k ∣ m * n) :

k ∣ 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.exists_coprime (m n : Nat) :

∃ (m' : Nat ), ∃ (n' : Nat ), m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

theorem Nat.exists_coprime' {m 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_left {m k n : Nat} (H1 : m.Coprime k) (H2 : n.Coprime k) :

(m * n).Coprime k

@[deprecated Nat.Coprime.mul_left (since := "2025-08-04")]

theorem Nat.Coprime.mul {m k n : Nat} (H1 : m.Coprime k) (H2 : n.Coprime k) :

(m * n).Coprime k

Alias of Nat.Coprime.mul_left.

theorem Nat.Coprime.mul_right {k m n : Nat} (H1 : k.Coprime m) (H2 : k.Coprime n) :

k.Coprime (m * 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_mul_left_right {m k n : Nat} (H : m.Coprime (k * n)) :

theorem Nat.Coprime.coprime_mul_right_right {m n k : Nat} (H : m.Coprime (n * k)) :

theorem Nat.Coprime.coprime_div_left {m n a : Nat} (cmn : m.Coprime n) (dvd : a ∣ m) :

(m / a).Coprime n

theorem Nat.Coprime.coprime_div_right {m n a : Nat} (cmn : m.Coprime n) (dvd : a ∣ n) :

m.Coprime (n / a)

theorem Nat.coprime_mul_iff_left {m n k : Nat} :

(m * n).Coprime k ↔ m.Coprime k ∧ n.Coprime k

theorem Nat.coprime_mul_iff_right {k m n : Nat} :

k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime 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) :

Coprime 0 n ↔ n = 1

@[simp]

theorem Nat.coprime_zero_right (n : Nat) :

n.Coprime 0 ↔ n = 1

theorem Nat.coprime_one_left (n : Nat) :

theorem Nat.coprime_one_right (n : Nat) :

@[simp]

theorem Nat.coprime_one_left_eq_true (n : Nat) :

Coprime 1 n = True

@[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 k : Nat} (n : Nat) (H1 : m.Coprime k) :

(m ^ n).Coprime k

theorem Nat.Coprime.pow_right {k m : Nat} (n : Nat) (H1 : k.Coprime m) :

k.Coprime (m ^ n)

theorem Nat.Coprime.pow {k l : Nat} (m n : Nat) (H1 : k.Coprime l) :

(k ^ m).Coprime (l ^ n)

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.Coprime.mul_gcd {m n : Nat} (h : m.Coprime n) (k : Nat) :

(m * n).gcd k = m.gcd k * n.gcd k

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