mathlib3 documentation

data.nat.prime

Prime numbers #

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

This file deals with prime numbers: natural numbers p ≥ 2 whose only divisors are p and 1.

Important declarations #

source
def nat.prime (p : ℕ) :
Prop

nat.prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1.

Equations
Instances for nat.prime
source
theorem irreducible_iff_nat_prime (a : ℕ) :
irreducible a ↔ nat.prime a
source
theorem nat.not_prime_zero  :
¬nat.prime 0
source
theorem nat.not_prime_one  :
¬nat.prime 1
source
theorem nat.prime.ne_zero {n : ℕ} (h : nat.prime n) :
n ≠ 0
source
theorem nat.prime.pos {p : ℕ} (pp : nat.prime p) :
0 < p
source
theorem nat.prime.two_le {p : ℕ} :
nat.prime p → 2 ≤ p
source
theorem nat.prime.one_lt {p : ℕ} :
nat.prime p → 1 < p
source
@[protected, instance]
def nat.prime.one_lt' (p : ℕ) [hp : fact (nat.prime p)] :
fact (1 < p)
source
theorem nat.prime.ne_one {p : ℕ} (hp : nat.prime p) :
p ≠ 1
source
theorem nat.prime.eq_one_or_self_of_dvd {p : ℕ} (pp : nat.prime p) (m : ℕ) (hm : m ∣ p) :
m = 1 ∨ m = p
source
theorem nat.prime_def_lt'' {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
source
theorem nat.prime_def_lt {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1
source
theorem nat.prime_def_lt' {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p
source
theorem nat.prime_def_le_sqrt {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ nat.sqrt p → ¬m ∣ p
source
theorem nat.prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ (m : ℕ), m < n → m ≠ 0 → n.coprime m) :
nat.prime n
source
def nat.decidable_prime_1 (p : ℕ) :
decidable (nat.prime p)

This instance is slower than the instance decidable_prime defined below, but has the advantage that it works in the kernel for small values.

If you need to prove that a particular number is prime, in any case you should not use dec_trivial, but rather by norm_num, which is much faster.

Equations
source
theorem nat.prime_two  :
nat.prime 2
source
theorem nat.prime_three  :
nat.prime 3
source
theorem nat.prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : nat.prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) :
5 ≤ p
source
theorem nat.prime.pred_pos {p : ℕ} (pp : nat.prime p) :
0 < p.pred
source
theorem nat.succ_pred_prime {p : ℕ} (pp : nat.prime p) :
p.pred.succ = p
source
theorem nat.dvd_prime {p m : ℕ} (pp : nat.prime p) :
m ∣ p ↔ m = 1 ∨ m = p
source
theorem nat.dvd_prime_two_le {p m : ℕ} (pp : nat.prime p) (H : 2 ≤ m) :
m ∣ p ↔ m = p
source
theorem nat.prime_dvd_prime_iff_eq {p q : ℕ} (pp : nat.prime p) (qp : nat.prime q) :
p ∣ q ↔ p = q
source
theorem nat.prime.not_dvd_one {p : ℕ} (pp : nat.prime p) :
¬p ∣ 1
source
theorem nat.not_prime_mul {a b : ℕ} (a1 : 1 < a) (b1 : 1 < b) :
¬nat.prime (a * b)
source
theorem nat.not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : 1 < a) (h₂ : 1 < b) :
¬nat.prime n
source
theorem nat.prime_mul_iff {a b : ℕ} :
nat.prime (a * b) ↔ nat.prime a ∧ b = 1 ∨ nat.prime b ∧ a = 1
source
theorem nat.prime.dvd_iff_eq {p a : ℕ} (hp : nat.prime p) (a1 : a ≠ 1) :
a ∣ p ↔ p = a
source
theorem nat.min_fac_lemma (n k : ℕ) (h : ¬n < k * k) :
nat.sqrt n - k < nat.sqrt n + 2 - k
source
def nat.min_fac_aux (n : ℕ) :
ℕ → ℕ

If n < k * k, then min_fac_aux n k = n, if k | n, then min_fac_aux n k = k. Otherwise, min_fac_aux n k = min_fac_aux n (k+2) using well-founded recursion. If n is odd and 1 < n, then then min_fac_aux n 3 is the smallest prime factor of n.

Equations
source
def nat.min_fac  :
ℕ → ℕ

Returns the smallest prime factor of n ≠ 1.

Equations
source
@[simp]
theorem nat.min_fac_zero  :
0.min_fac = 2
source
@[simp]
theorem nat.min_fac_one  :
1.min_fac = 1
source
theorem nat.min_fac_eq (n : ℕ) :
n.min_fac = ite (2 ∣ n) 2 (n.min_fac_aux 3)
source
theorem nat.min_fac_aux_has_prop {n : ℕ} (n2 : 2 ≤ n) (k i : ℕ) :
k = 2 * i + 3 → (∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m) → min_fac_prop n (n.min_fac_aux k)
source
theorem nat.min_fac_has_prop {n : ℕ} (n1 : n ≠ 1) :
min_fac_prop n n.min_fac
source
theorem nat.min_fac_dvd (n : ℕ) :
n.min_fac ∣ n
source
theorem nat.min_fac_prime {n : ℕ} (n1 : n ≠ 1) :
nat.prime n.min_fac
source
theorem nat.min_fac_le_of_dvd {n m : ℕ} :
2 ≤ m → m ∣ n → n.min_fac ≤ m
source
theorem nat.min_fac_pos (n : ℕ) :
0 < n.min_fac
source
theorem nat.min_fac_le {n : ℕ} (H : 0 < n) :
n.min_fac ≤ n
source
theorem nat.le_min_fac {m n : ℕ} :
n = 1 ∨ m ≤ n.min_fac ↔ ∀ (p : ℕ), nat.prime p → p ∣ n → m ≤ p
source
theorem nat.le_min_fac' {m n : ℕ} :
n = 1 ∨ m ≤ n.min_fac ↔ ∀ (p : ℕ), 2 ≤ p → p ∣ n → m ≤ p
source
theorem nat.prime_def_min_fac {p : ℕ} :
nat.prime p ↔ 2 ≤ p ∧ p.min_fac = p
source
@[simp]
theorem nat.prime.min_fac_eq {p : ℕ} (hp : nat.prime p) :
p.min_fac = p
source
@[protected, instance]
def nat.decidable_prime (p : ℕ) :
decidable (nat.prime p)

This instance is faster in the virtual machine than decidable_prime_1, but slower in the kernel.

If you need to prove that a particular number is prime, in any case you should not use dec_trivial, but rather by norm_num, which is much faster.

Equations
source
theorem nat.not_prime_iff_min_fac_lt {n : ℕ} (n2 : 2 ≤ n) :
¬nat.prime n ↔ n.min_fac < n
source
theorem nat.min_fac_le_div {n : ℕ} (pos : 0 < n) (np : ¬nat.prime n) :
n.min_fac ≤ n / n.min_fac
source
theorem nat.min_fac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬nat.prime n) :
n.min_fac ^ 2 ≤ n

The square of the smallest prime factor of a composite number n is at most n.

source
@[simp]
theorem nat.min_fac_eq_one_iff {n : ℕ} :
n.min_fac = 1 ↔ n = 1
source
@[simp]
theorem nat.min_fac_eq_two_iff (n : ℕ) :
n.min_fac = 2 ↔ 2 ∣ n
source
theorem nat.exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬nat.prime n) :
∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n
source
theorem nat.exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬nat.prime n) :
∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n
source
theorem nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) :
∃ (p : ℕ), nat.prime p ∧ p ∣ n
source
theorem nat.dvd_of_forall_prime_mul_dvd {a b : ℕ} (hdvd : ∀ (p : ℕ), nat.prime p → p ∣ a → p * a ∣ b) :
a ∣ b
source
theorem nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ nat.prime p

Euclid's theorem on the infinitude of primes. Here given in the form: for every n, there exists a prime number p ≥ n.

source
theorem nat.not_bdd_above_set_of_prime  :
¬bdd_above {p : ℕ | nat.prime p}

A version of nat.exists_infinite_primes using the bdd_above predicate.

source
theorem nat.prime.eq_two_or_odd {p : ℕ} (hp : nat.prime p) :
p = 2 ∨ p % 2 = 1
source
theorem nat.prime.eq_two_or_odd' {p : ℕ} (hp : nat.prime p) :
p = 2 ∨ odd p
source
theorem nat.prime.even_iff {p : ℕ} (hp : nat.prime p) :
even p ↔ p = 2
source
theorem nat.prime.odd_of_ne_two {p : ℕ} (hp : nat.prime p) (h_two : p ≠ 2) :
odd p
source
theorem nat.prime.even_sub_one {p : ℕ} (hp : nat.prime p) (h2 : p ≠ 2) :
even (p - 1)
source
theorem nat.prime.mod_two_eq_one_iff_ne_two {p : ℕ} [fact (nat.prime p)] :
p % 2 = 1 ↔ p ≠ 2

A prime p satisfies p % 2 = 1 if and only if p ≠ 2.

source
theorem nat.coprime_of_dvd {m n : ℕ} (H : ∀ (k : ℕ), nat.prime k → k ∣ m → ¬k ∣ n) :
m.coprime n
source
theorem nat.coprime_of_dvd' {m n : ℕ} (H : ∀ (k : ℕ), nat.prime k → k ∣ m → k ∣ n → k ∣ 1) :
m.coprime n
source
theorem nat.factors_lemma {k : ℕ} :
(k + 2) / (k + 2).min_fac < k + 2
source
theorem nat.prime.coprime_iff_not_dvd {p n : ℕ} (pp : nat.prime p) :
p.coprime n ↔ ¬p ∣ n
source
theorem nat.prime.dvd_iff_not_coprime {p n : ℕ} (pp : nat.prime p) :
p ∣ n ↔ ¬p.coprime n
source
theorem nat.prime.not_coprime_iff_dvd {m n : ℕ} :
¬m.coprime n ↔ ∃ (p : ℕ), nat.prime p ∧ p ∣ m ∧ p ∣ n
source
theorem nat.prime.dvd_mul {p m n : ℕ} (pp : nat.prime p) :
p ∣ m * n ↔ p ∣ m ∨ p ∣ n
source
theorem nat.prime.not_dvd_mul {p m n : ℕ} (pp : nat.prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) :
¬p ∣ m * n
source
theorem nat.prime_iff {p : ℕ} :
nat.prime p ↔ prime p
source
theorem prime.nat_prime {p : ℕ} :
prime p → nat.prime p

Alias of the reverse direction of nat.prime_iff.

source
@[protected, nolint]
theorem nat.prime.prime {p : ℕ} :
nat.prime p → prime p

Alias of the forward direction of nat.prime_iff.

source
theorem nat.irreducible_iff_prime {p : ℕ} :
irreducible p ↔ prime p
source
theorem nat.prime.dvd_of_dvd_pow {p m n : ℕ} (pp : nat.prime p) (h : p ∣ m ^ n) :
p ∣ m
source
theorem nat.prime.pow_not_prime {x n : ℕ} (hn : 2 ≤ n) :
¬nat.prime (x ^ n)
source
theorem nat.prime.pow_not_prime' {x n : ℕ} :
n ≠ 1 → ¬nat.prime (x ^ n)
source
theorem nat.prime.eq_one_of_pow {x n : ℕ} (h : nat.prime (x ^ n)) :
n = 1
source
theorem nat.prime.pow_eq_iff {p a k : ℕ} (hp : nat.prime p) :
a ^ k = p ↔ a = p ∧ k = 1
source
theorem nat.pow_min_fac {n k : ℕ} (hk : k ≠ 0) :
(n ^ k).min_fac = n.min_fac
source
theorem nat.prime.pow_min_fac {p k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) :
(p ^ k).min_fac = p
source
theorem nat.prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : nat.prime p) (hx : x ≠ 1) (hy : y ≠ 1) :
x * y = p ^ 2 ↔ x = p ∧ y = p
source
theorem nat.prime.dvd_factorial {n p : ℕ} (hp : nat.prime p) :
p ∣ n.factorial ↔ p ≤ n
source
theorem nat.prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : nat.prime p) (h : ¬p ∣ a) :
a.coprime (p ^ m)
source
theorem nat.coprime_primes {p q : ℕ} (pp : nat.prime p) (pq : nat.prime q) :
p.coprime q ↔ p ≠ q
source
theorem nat.coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : nat.prime p) (pq : nat.prime q) (h : p ≠ q) :
(p ^ n).coprime (q ^ m)
source
theorem nat.coprime_or_dvd_of_prime {p : ℕ} (pp : nat.prime p) (i : ℕ) :
p.coprime i ∨ p ∣ i
source
theorem nat.coprime_of_lt_prime {n p : ℕ} (n_pos : 0 < n) (hlt : n < p) (pp : nat.prime p) :
p.coprime n
source
theorem nat.eq_or_coprime_of_le_prime {n p : ℕ} (n_pos : 0 < n) (hle : n ≤ p) (pp : nat.prime p) :
p = n ∨ p.coprime n
source
theorem nat.dvd_prime_pow {p : ℕ} (pp : nat.prime p) {m i : ℕ} :
i ∣ p ^ m ↔ ∃ (k : ℕ) (H : k ≤ m), i = p ^ k
source
theorem nat.prime.dvd_mul_of_dvd_ne {p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : nat.prime p1) (pp2 : nat.prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) :
p1 * p2 ∣ n
source
theorem nat.eq_prime_pow_of_dvd_least_prime_pow {a p k : ℕ} (pp : nat.prime p) (h₁ : ¬a ∣ p ^ k) (h₂ : a ∣ p ^ (k + 1)) :
a = p ^ (k + 1)

If p is prime, and a doesn't divide p^k, but a does divide p^(k+1) then a = p^(k+1).

source
theorem nat.ne_one_iff_exists_prime_dvd {n : ℕ} :
n ≠ 1 ↔ ∃ (p : ℕ), nat.prime p ∧ p ∣ n
source
theorem nat.eq_one_iff_not_exists_prime_dvd {n : ℕ} :
n = 1 ↔ ∀ (p : ℕ), nat.prime p → ¬p ∣ n
source
theorem nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n k l : ℕ} (hpm : p ^ k ∣ m) (hpn : p ^ l ∣ n) (hpmn : p ^ (k + l + 1) ∣ m * n) :
p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
source
theorem nat.prime_iff_prime_int {p : ℕ} :
nat.prime p ↔ prime ↑p
source
def nat.primes  :
Type

The type of prime numbers

Equations
Instances for nat.primes
source
@[protected, instance]
def nat.primes.has_repr  :
has_repr nat.primes
Equations
source
@[protected, instance]
def nat.primes.inhabited_primes  :
inhabited nat.primes
Equations
source
@[protected, instance]
def nat.primes.coe_nat  :
has_coe nat.primes ℕ
Equations
source
theorem nat.primes.coe_nat_injective  :
function.injective coe
source
theorem nat.primes.coe_nat_inj (p q : nat.primes) :
↑p = ↑q ↔ p = q
source
@[protected, instance]
def nat.monoid.prime_pow {α : Type u_1} [monoid α] :
has_pow α nat.primes
Equations
source
@[protected, instance]
def nat.fact_prime_two  :
fact (nat.prime 2)
source
@[protected, instance]
def nat.fact_prime_three  :
fact (nat.prime 3)
source
theorem int.prime_two  :
prime 2
source
theorem int.prime_three  :
prime 3