data.pnat.prime

# Primality and GCD on pnat #

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

@[protected, instance]
Equations
theorem nat.primes.coe_pnat_inj (p q : nat.primes) :
p = qp = q
def pnat.gcd (n m : ℕ+) :

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

Equations
def pnat.lcm (n m : ℕ+) :

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

Equations
@[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 : ℕ+) :
Prop

Primality predicate for ℕ+, defined in terms of nat.prime.

Equations
theorem pnat.prime.one_lt {p : ℕ+} :
p.prime1 < p
theorem pnat.prime_two  :
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.not_prime_one  :
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 : ℕ+) :
Prop

Two pnats are coprime if their gcd is 1.

Equations
@[simp]
theorem pnat.coprime_coe {m 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 : ℕ+} :
1.gcd n = 1
@[simp]
theorem pnat.gcd_one {n : ℕ+} :
n.gcd 1 = 1
@[symm]
theorem pnat.coprime.symm {m n : ℕ+} :
m.coprime nn.coprime m
@[simp]
theorem pnat.one_coprime {n : ℕ+} :
@[simp]
theorem pnat.coprime_one {n : ℕ+} :
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)