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 : Primes → ℕ+

The canonical map from Nat.Primes to ℕ+

instance Nat.Primes.coePNat : Coe Primes ℕ+

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

theorem Nat.Primes.coe_pnat_injective : Function.Injective toPNat

theorem Nat.Primes.coe_pnat_inj (p q : 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.

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

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

@[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 < 2 → n = 1

Prime numbers

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

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

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

theorem PNat.prime_two : Prime 2

instance PNat.instFactPrimeValOfPrime {p : ℕ+} [h : Fact p.Prime] : Fact (Nat.Prime ↑p)

instance PNat.fact_prime_two : Fact (Prime 2)

theorem PNat.prime_three : Prime 3

instance PNat.fact_prime_three : Fact (Prime 3)

theorem PNat.prime_five : Prime 5

instance PNat.fact_prime_five : Fact (Prime 5)

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

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

@[simp]

theorem PNat.not_prime_one : ¬Prime 1

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.

@[simp]

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

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

theorem PNat.Coprime.mul_right {k m n : ℕ+} : k.Coprime m → k.Coprime n → k.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.gcd n = m ↔ m ∣ n

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

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 m → m.gcd (k * n) = m.gcd n

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem PNat.Coprime.coprime_dvd_left {m k n : ℕ+} : m ∣ k → k.Coprime n → m.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

@[deprecated PNat.gcd_eq_left_iff_dvd (since := "2025-11-14")]

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

Alias of the reverse direction of PNat.gcd_eq_left_iff_dvd.

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