# Primality and GCD on pnat #

This file extends the theory of ℕ+ with gcd, lcm and Prime functions, analogous to those on Nat.

The canonical map from Nat.Primes to ℕ+

Equations
• p = p,
Instances For
theorem Nat.Primes.coe_pnat_nat (p : Nat.Primes) :
p = p
theorem Nat.Primes.coe_pnat_inj (p : Nat.Primes) (q : Nat.Primes) :
p = q p = q
def PNat.gcd (n : ℕ+) (m : ℕ+) :

The greatest common divisor (gcd) of two positive natural numbers, viewed as positive natural number.

Equations
• n.gcd m = (↑n).gcd m,
Instances For
def PNat.lcm (n : ℕ+) (m : ℕ+) :

The least common multiple (lcm) of two positive natural numbers, viewed as positive natural number.

Equations
• n.lcm m = (↑n).lcm m,
Instances For
@[simp]
theorem PNat.gcd_coe (n : ℕ+) (m : ℕ+) :
(n.gcd m) = (↑n).gcd m
@[simp]
theorem PNat.lcm_coe (n : ℕ+) (m : ℕ+) :
(n.lcm m) = (↑n).lcm m
theorem PNat.gcd_dvd_left (n : ℕ+) (m : ℕ+) :
n.gcd m n
theorem PNat.gcd_dvd_right (n : ℕ+) (m : ℕ+) :
n.gcd m m
theorem PNat.dvd_gcd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : k m) (hn : k n) :
k m.gcd n
theorem PNat.dvd_lcm_left (n : ℕ+) (m : ℕ+) :
n n.lcm m
theorem PNat.dvd_lcm_right (n : ℕ+) (m : ℕ+) :
m n.lcm m
theorem PNat.lcm_dvd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : m k) (hn : n k) :
m.lcm n k
theorem PNat.gcd_mul_lcm (n : ℕ+) (m : ℕ+) :
n.gcd m * n.lcm m = n * m
theorem PNat.eq_one_of_lt_two {n : ℕ+} :
n < 2n = 1

### Prime numbers #

def PNat.Prime (p : ℕ+) :

Primality predicate for ℕ+, defined in terms of Nat.Prime.

Equations
• p.Prime =
Instances For
theorem PNat.Prime.one_lt {p : ℕ+} :
p.Prime1 < p
instance PNat.instFactPrimeValOfPrime {p : ℕ+} [h : Fact p.Prime] :
Equations
• = h
theorem PNat.dvd_prime {p : ℕ+} {m : ℕ+} (pp : p.Prime) :
m p m = 1 m = p
theorem PNat.Prime.ne_one {p : ℕ+} :
p.Primep 1
@[simp]
theorem PNat.Prime.not_dvd_one {p : ℕ+} :
p.Prime¬p 1
theorem PNat.exists_prime_and_dvd {n : ℕ+} (hn : n 1) :
∃ (p : ℕ+), p.Prime p n

### Coprime numbers and gcd #

def PNat.Coprime (m : ℕ+) (n : ℕ+) :

Two pnats are coprime if their gcd is 1.

Equations
• m.Coprime n = (m.gcd n = 1)
Instances For
@[simp]
theorem PNat.coprime_coe {m : ℕ+} {n : ℕ+} :
(↑m).Coprime n m.Coprime n
theorem PNat.Coprime.mul {k : ℕ+} {m : ℕ+} {n : ℕ+} :
m.Coprime kn.Coprime k(m * n).Coprime k
theorem PNat.Coprime.mul_right {k : ℕ+} {m : ℕ+} {n : ℕ+} :
k.Coprime mk.Coprime nk.Coprime (m * n)
theorem PNat.gcd_comm {m : ℕ+} {n : ℕ+} :
m.gcd n = n.gcd m
theorem PNat.gcd_eq_left_iff_dvd {m : ℕ+} {n : ℕ+} :
m n m.gcd n = m
theorem PNat.gcd_eq_right_iff_dvd {m : ℕ+} {n : ℕ+} :
m n n.gcd m = m
theorem PNat.Coprime.gcd_mul_left_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
k.Coprime n(k * m).gcd n = m.gcd n
theorem PNat.Coprime.gcd_mul_right_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
k.Coprime n(m * k).gcd n = m.gcd n
theorem PNat.Coprime.gcd_mul_left_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} :
k.Coprime mm.gcd (k * n) = m.gcd n
theorem PNat.Coprime.gcd_mul_right_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} :
k.Coprime mm.gcd (n * k) = m.gcd n
@[simp]
theorem PNat.one_gcd {n : ℕ+} :
PNat.gcd 1 n = 1
@[simp]
theorem PNat.gcd_one {n : ℕ+} :
n.gcd 1 = 1
theorem PNat.Coprime.symm {m : ℕ+} {n : ℕ+} :
m.Coprime nn.Coprime m
@[simp]
theorem PNat.one_coprime {n : ℕ+} :
@[simp]
theorem PNat.coprime_one {n : ℕ+} :
n.Coprime 1
theorem PNat.Coprime.coprime_dvd_left {m : ℕ+} {k : ℕ+} {n : ℕ+} :
m kk.Coprime nm.Coprime n
theorem PNat.Coprime.factor_eq_gcd_left {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
a = (a * b).gcd m
theorem PNat.Coprime.factor_eq_gcd_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
a = (b * a).gcd m
theorem PNat.Coprime.factor_eq_gcd_left_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
a = m.gcd (a * b)
theorem PNat.Coprime.factor_eq_gcd_right_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
a = m.gcd (b * a)
theorem PNat.Coprime.gcd_mul (k : ℕ+) {m : ℕ+} {n : ℕ+} (h : m.Coprime n) :
k.gcd (m * n) = k.gcd m * k.gcd n
theorem PNat.gcd_eq_left {m : ℕ+} {n : ℕ+} :
m nm.gcd n = m
theorem PNat.Coprime.pow {m : ℕ+} {n : ℕ+} (k : ) (l : ) (h : m.Coprime n) :
(m ^ k).Coprime (n ^ l)