# Primality and GCD on pnat #

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

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

The canonical map from `Nat.Primes` to `ℕ+`

Equations

- ↑p = ⟨↑p, ⋯⟩

Instances For

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

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

source
theorem Nat.Primes.coe_pnat_nat (p : Primes) :
↑↑p = ↑p
source
theorem Nat.Primes.coe_pnat_injective :
Function.Injective toPNat
source
theorem Nat.Primes.coe_pnat_inj (p q : Primes) :
↑p = ↑q ↔ p = q
source
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

source
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

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

### Prime numbers #

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

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

Equations

- p.Prime = Nat.Prime ↑p

Instances For

source
theorem PNat.Prime.one_lt {p : ℕ+} :
p.Prime → 1 < p
source
theorem PNat.prime_two :
Prime 2
source
instance PNat.instFactPrimeValOfPrime {p : ℕ+} [h : Fact p.Prime] :
Fact (Nat.Prime ↑p)
source
instance PNat.fact_prime_two :
Fact (Prime 2)
source
theorem PNat.prime_three :
Prime 3
source
instance PNat.fact_prime_three :
Fact (Prime 3)
source
theorem PNat.prime_five :
Prime 5
source
instance PNat.fact_prime_five :
Fact (Prime 5)
source
theorem PNat.dvd_prime {p m : ℕ+} (pp : p.Prime) :
m ∣ p ↔ m = 1 ∨ m = p
source
theorem PNat.Prime.ne_one {p : ℕ+} :
p.Prime → p ≠ 1
source
@[simp]
theorem PNat.not_prime_one :
¬Prime 1
source
theorem PNat.Prime.not_dvd_one {p : ℕ+} :
p.Prime → ¬p ∣ 1
source
theorem PNat.exists_prime_and_dvd {n : ℕ+} (hn : n ≠ 1) :
∃ (p : ℕ+), p.Prime ∧ p ∣ n

### Coprime numbers and gcd #

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

Two pnats are coprime if their gcd is 1.

Equations

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

Instances For

source
@[simp]
theorem PNat.coprime_coe {m n : ℕ+} :
(↑m).Coprime ↑n ↔ m.Coprime n
source
theorem PNat.Coprime.mul {k m n : ℕ+} :
m.Coprime k → n.Coprime k → (m * n).Coprime k
source
theorem PNat.Coprime.mul_right {k m n : ℕ+} :
k.Coprime m → k.Coprime n → k.Coprime (m * n)
source
theorem PNat.gcd_comm {m n : ℕ+} :
m.gcd n = n.gcd m
source
theorem PNat.gcd_eq_left_iff_dvd {m n : ℕ+} :
m.gcd n = m ↔ m ∣ n
source
theorem PNat.gcd_eq_right_iff_dvd {m n : ℕ+} :
n.gcd m = m ↔ m ∣ n
source
theorem PNat.Coprime.gcd_mul_left_cancel (m : ℕ+) {n k : ℕ+} :
k.Coprime n → (k * m).gcd n = m.gcd n
source
theorem PNat.Coprime.gcd_mul_right_cancel (m : ℕ+) {n k : ℕ+} :
k.Coprime n → (m * k).gcd n = m.gcd n
source
theorem PNat.Coprime.gcd_mul_left_cancel_right (m : ℕ+) {n k : ℕ+} :
k.Coprime m → m.gcd (k * n) = m.gcd n
source
theorem PNat.Coprime.gcd_mul_right_cancel_right (m : ℕ+) {n k : ℕ+} :
k.Coprime m → m.gcd (n * k) = m.gcd n
source
@[simp]
theorem PNat.one_gcd {n : ℕ+} :
gcd 1 n = 1
source
@[simp]
theorem PNat.gcd_one {n : ℕ+} :
n.gcd 1 = 1
source
theorem PNat.Coprime.symm {m n : ℕ+} :
m.Coprime n → n.Coprime m
source
@[simp]
theorem PNat.one_coprime {n : ℕ+} :
Coprime 1 n
source
@[simp]
theorem PNat.coprime_one {n : ℕ+} :
n.Coprime 1
source
theorem PNat.Coprime.coprime_dvd_left {m k n : ℕ+} :
m ∣ k → k.Coprime n → m.Coprime n
source
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
source
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
source
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)
source
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)
source
theorem PNat.Coprime.gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.Coprime n) :
k.gcd (m * n) = k.gcd m * k.gcd n
source
@[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`.

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