Prime numbers

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

Important declarations

All the following declarations exist in the namespace nat.

prime: the predicate that expresses that a natural number p is prime
primes: the subtype of natural numbers that are prime
min_fac n: the minimal prime factor of a natural number n ≠ 1
exists_infinite_primes: Euclid's theorem that there exist infinitely many prime numbers
factors n: the prime factorization of n
factors_unique: uniqueness of the prime factorisation

source

def nat.prime (p : ℕ) :

Prop

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

nat.prime p = (2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p)

source

theorem nat.prime.two_le {p : ℕ} (a : nat.prime p) :

2 ≤ p

source

theorem nat.prime.one_lt {p : ℕ} (a : nat.prime p) :

1 < p

source

@[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_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

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.

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

p.decidable_prime_1 = decidable_of_iff' (2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) nat.prime_def_lt'

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.not_prime_zero :

¬nat.prime 0

source

theorem nat.not_prime_one :

¬nat.prime 1

source

theorem nat.prime_two :

nat.prime 2

source

theorem nat.prime_three :

nat.prime 3

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

def nat.min_fac_aux (n a : ℕ) :

ℕ

Equations

n.min_fac_aux k = ite (n < k * k) n (ite (k ∣ n) k (n.min_fac_aux (k + 2)))

source

def nat.min_fac (a : ℕ) :

ℕ

Returns the smallest prime factor of n ≠ 1.

Equations

(n + 2).min_fac = ite (2 ∣ n) 2 ((n + 2).min_fac_aux 3)
1.min_fac = 1
0.min_fac = 2

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) (nd2 : ¬2 ∣ n) (k i : ℕ) (a : k = 2 * i + 3) (a_1 : ∀ (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 : ℕ} (a : 2 ≤ m) (a_1 : 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.prime_def_min_fac {p : ℕ} :

nat.prime p ↔ 2 ≤ p ∧ p.min_fac = p

source

@[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

p.decidable_prime = decidable_of_iff' (2 ≤ p ∧ p.min_fac = p) nat.prime_def_min_fac

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 : ℕ} (n2 : 2 ≤ n) :

∃ (p : ℕ), nat.prime p ∧ p ∣ n

source

theorem nat.exists_infinite_primes (n : ℕ) :

∃ (p : ℕ), n ≤ p ∧ nat.prime p

Euclid's theorem. There exist infinitely many prime numbers. Here given in the form: for every n, there exists a prime number p ≥ n.

source

theorem nat.prime.eq_two_or_odd {p : ℕ} (hp : nat.prime p) :

p = 2 ∨ p % 2 = 1

source

theorem nat.factors_lemma {k : ℕ} :

(k + 2) / (k + 2).min_fac < k + 2

source

def nat.factors (a : ℕ) :

list ℕ

factors n is the prime factorization of n, listed in increasing order.

Equations

(k + 2).factors = let m : ℕ := (k + 2).min_fac in m :: ((k + 2) / m).factors
1.factors = list.nil
0.factors = list.nil

source

theorem nat.mem_factors {n p : ℕ} (a : p ∈ n.factors) :

nat.prime p

source

theorem nat.prod_factors {n : ℕ} (a : 0 < n) :

n.factors.prod = n

source

theorem nat.factors_prime {p : ℕ} (hp : nat.prime p) :

p.factors = [p]

source

theorem nat.factors_add_two (n : ℕ) :

(n + 2).factors = (n + 2).min_fac :: ((n + 2) / (n + 2).min_fac).factors

factors can be constructed inductively by extracting min_fac, for sufficiently large n.

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.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.mul_eq_prime_pow_two_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_fact {n p : ℕ} (hp : nat.prime p) :

p ∣ n.fact ↔ 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.dvd_prime_pow {p : ℕ} (pp : nat.prime p) {m i : ℕ} :

i ∣ p ^ m ↔ ∃ (k : ℕ) (H : k ≤ m), i = p ^ k

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.mem_list_primes_of_dvd_prod {p : ℕ} (hp : nat.prime p) {l : list ℕ} (a : ∀ (p : ℕ), p ∈ l → nat.prime p) (a_1 : p ∣ l.prod) :

p ∈ l

source

theorem nat.mem_factors_iff_dvd {n p : ℕ} (hn : 0 < n) (hp : nat.prime p) :

p ∈ n.factors ↔ p ∣ n

source

theorem nat.perm_of_prod_eq_prod {l₁ l₂ : list ℕ} (a : l₁.prod = l₂.prod) (a_1 : ∀ (p : ℕ), p ∈ l₁ → nat.prime p) (a_2 : ∀ (p : ℕ), p ∈ l₂ → nat.prime p) :

l₁ ~ l₂

source

theorem nat.factors_unique {n : ℕ} {l : list ℕ} (h₁ : l.prod = n) (h₂ : ∀ (p : ℕ), p ∈ l → nat.prime p) :

l ~ n.factors

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

def nat.primes :

Type

The type of prime numbers

Equations