mathlib3 documentation

data.pnat.prime

Primality and GCD on pnat #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[protected, instance]
def nat.primes.coe_pnat  :
has_coe nat.primes ℕ+
Equations
source
@[norm_cast]
theorem nat.primes.coe_pnat_nat (p : nat.primes) :
↑↑p = ↑p
source
theorem nat.primes.coe_pnat_injective  :
function.injective coe
source
@[norm_cast]
theorem nat.primes.coe_pnat_inj (p q : nat.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
source
def pnat.lcm (n m : ℕ+) :
ℕ+

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

Equations
source
@[simp, norm_cast]
theorem pnat.gcd_coe (n m : ℕ+) :
↑(n.gcd m) = ↑n.gcd ↑m
source
@[simp, norm_cast]
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
source
theorem pnat.prime.one_lt {p : ℕ+} :
p.prime → 1 < p
source
theorem pnat.prime_two  :
2.prime
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  :
¬1.prime
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
source
@[simp, norm_cast]
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 ∣ n ↔ m.gcd n = m
source
theorem pnat.gcd_eq_right_iff_dvd {m n : ℕ+} :
m ∣ n ↔ n.gcd m = m
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 : ℕ+} :
1.gcd n = 1
source
@[simp]
theorem pnat.gcd_one {n : ℕ+} :
n.gcd 1 = 1
source
@[symm]
theorem pnat.coprime.symm {m n : ℕ+} :
m.coprime n → n.coprime m
source
@[simp]
theorem pnat.one_coprime {n : ℕ+} :
1.coprime 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
theorem pnat.gcd_eq_left {m n : ℕ+} :
m ∣ n → m.gcd n = m
source
theorem pnat.coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.coprime n) :
(m ^ k).coprime (n ^ l)