Primality and GCD on pnat

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

def Nat.Primes.toPNat : Nat.Primes → ℕ+

The canonical map from Nat.Primes to ℕ+

Equations

• ↑p = { val := ↑p, property := (_ : 0 < ↑p) }

instance Nat.Primes.coePNat : Coe Nat.Primes ℕ+

Equations

• Nat.Primes.coePNat = { coe := Nat.Primes.toPNat }

theorem Nat.Primes.coe_pnat_nat (p : Nat.Primes) : ↑↑p = ↑p

theorem Nat.Primes.coe_pnat_injective : Function.Injective Nat.Primes.toPNat

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

• PNat.gcd n m = { val := Nat.gcd ↑n ↑m, property := (_ : 0 < Nat.gcd ↑n ↑m) }

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

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

Equations

• PNat.lcm n m = { val := Nat.lcm ↑n ↑m, property := (_ : 0 < Nat.lcm ↑n ↑m) }

@[simp]

theorem PNat.gcd_coe (n : ℕ+) (m : ℕ+) : ↑(PNat.gcd n m) = Nat.gcd ↑n ↑m

@[simp]

theorem PNat.lcm_coe (n : ℕ+) (m : ℕ+) : ↑(PNat.lcm n m) = Nat.lcm ↑n ↑m

theorem PNat.gcd_dvd_left (n : ℕ+) (m : ℕ+) : PNat.gcd n m ∣ n

theorem PNat.gcd_dvd_right (n : ℕ+) (m : ℕ+) : PNat.gcd n m ∣ m

theorem PNat.dvd_gcd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : k ∣ m) (hn : k ∣ n) : k ∣ PNat.gcd m n

theorem PNat.dvd_lcm_left (n : ℕ+) (m : ℕ+) : n ∣ PNat.lcm n m

theorem PNat.dvd_lcm_right (n : ℕ+) (m : ℕ+) : m ∣ PNat.lcm n m

theorem PNat.lcm_dvd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : m ∣ k) (hn : n ∣ k) : PNat.lcm m n ∣ k

theorem PNat.gcd_mul_lcm (n : ℕ+) (m : ℕ+) : PNat.gcd n m * PNat.lcm n m = n * m

theorem PNat.eq_one_of_lt_two {n : ℕ+} : n < 2 → n = 1

Prime numbers

def PNat.Prime (p : ℕ+) : Prop

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

Equations

• PNat.Prime p = Nat.Prime ↑p

theorem PNat.Prime.one_lt {p : ℕ+} : PNat.Prime p → 1 < p

theorem PNat.prime_two : PNat.Prime 2

theorem PNat.dvd_prime {p : ℕ+} {m : ℕ+} (pp : PNat.Prime p) : m ∣ p ↔ m = 1 ∨ m = p

theorem PNat.Prime.ne_one {p : ℕ+} : PNat.Prime p → p ≠ 1

@[simp]

theorem PNat.not_prime_one : ¬PNat.Prime 1

theorem PNat.Prime.not_dvd_one {p : ℕ+} : PNat.Prime p → ¬p ∣ 1

theorem PNat.exists_prime_and_dvd {n : ℕ+} (hn : n ≠ 1) : ∃ p, PNat.Prime p ∧ p ∣ n

Coprime numbers and gcd

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

Two pnats are coprime if their gcd is 1.

Equations

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

@[simp]

theorem PNat.coprime_coe {m : ℕ+} {n : ℕ+} : Nat.Coprime ↑m ↑n ↔ PNat.Coprime m n

theorem PNat.Coprime.mul {k : ℕ+} {m : ℕ+} {n : ℕ+} : PNat.Coprime m k → PNat.Coprime n k → PNat.Coprime (m * n) k

theorem PNat.Coprime.mul_right {k : ℕ+} {m : ℕ+} {n : ℕ+} : PNat.Coprime k m → PNat.Coprime k n → PNat.Coprime k (m * n)

theorem PNat.gcd_comm {m : ℕ+} {n : ℕ+} : PNat.gcd m n = PNat.gcd n m

theorem PNat.gcd_eq_left_iff_dvd {m : ℕ+} {n : ℕ+} : m ∣ n ↔ PNat.gcd m n = m

theorem PNat.gcd_eq_right_iff_dvd {m : ℕ+} {n : ℕ+} : m ∣ n ↔ PNat.gcd n m = m

theorem PNat.Coprime.gcd_mul_left_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} : PNat.Coprime k n → PNat.gcd (k * m) n = PNat.gcd m n

theorem PNat.Coprime.gcd_mul_right_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} : PNat.Coprime k n → PNat.gcd (m * k) n = PNat.gcd m n

theorem PNat.Coprime.gcd_mul_left_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} : PNat.Coprime k m → PNat.gcd m (k * n) = PNat.gcd m n

theorem PNat.Coprime.gcd_mul_right_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} : PNat.Coprime k m → PNat.gcd m (n * k) = PNat.gcd m n

@[simp]

theorem PNat.one_gcd {n : ℕ+} : PNat.gcd 1 n = 1

@[simp]

theorem PNat.gcd_one {n : ℕ+} : PNat.gcd n 1 = 1

theorem PNat.Coprime.symm {m : ℕ+} {n : ℕ+} : PNat.Coprime m n → PNat.Coprime n m

@[simp]

theorem PNat.one_coprime {n : ℕ+} : PNat.Coprime 1 n

@[simp]

theorem PNat.coprime_one {n : ℕ+} : PNat.Coprime n 1

theorem PNat.Coprime.coprime_dvd_left {m : ℕ+} {k : ℕ+} {n : ℕ+} : m ∣ k → PNat.Coprime k n → PNat.Coprime m n

theorem PNat.Coprime.factor_eq_gcd_left {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a ∣ m) (bn : b ∣ n) : a = PNat.gcd (a * b) m

theorem PNat.Coprime.factor_eq_gcd_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a ∣ m) (bn : b ∣ n) : a = PNat.gcd (b * a) m

theorem PNat.Coprime.factor_eq_gcd_left_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a ∣ m) (bn : b ∣ n) : a = PNat.gcd m (a * b)

theorem PNat.Coprime.factor_eq_gcd_right_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a ∣ m) (bn : b ∣ n) : a = PNat.gcd m (b * a)

theorem PNat.Coprime.gcd_mul (k : ℕ+) {m : ℕ+} {n : ℕ+} (h : PNat.Coprime m n) : PNat.gcd k (m * n) = PNat.gcd k m * PNat.gcd k n

theorem PNat.gcd_eq_left {m : ℕ+} {n : ℕ+} : m ∣ n → PNat.gcd m n = m

theorem PNat.Coprime.pow {m : ℕ+} {n : ℕ+} (k : ℕ) (l : ℕ) (h : PNat.Coprime m n) : Nat.Coprime (↑m ^ k) (↑n ^ l)