data.nat.prime

# 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
def nat.prime  :
→ 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
theorem nat.prime.two_le {p : } :
2 p

theorem nat.prime.one_lt {p : } :
1 < p

@[instance]
def nat.prime.one_lt' (p : ) [hp : fact (nat.prime p)] :
fact (1 < p)

theorem nat.prime.ne_one {p : } :
p 1

theorem nat.prime_def_lt {p : } :
2 p ∀ (m : ), m < pm pm = 1

theorem nat.prime_def_lt' {p : } :
2 p ∀ (m : ), 2 mm < p¬m p

theorem nat.prime_def_le_sqrt {p : } :
2 p ∀ (m : ), 2 mm ¬m p

def nat.decidable_prime_1 (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
theorem nat.prime.ne_zero {n : } :
n 0

theorem nat.prime.pos {p : } :
0 < p

theorem nat.prime_two  :

theorem nat.prime_three  :

theorem nat.prime.pred_pos {p : } :
0 < p.pred

theorem nat.succ_pred_prime {p : } :
p.pred.succ = p

theorem nat.dvd_prime {p m : } :
(m p m = 1 m = p)

theorem nat.dvd_prime_two_le {p m : } :
2 m(m p m = p)

theorem nat.prime_dvd_prime_iff_eq {p q : } :
(p q p = q)

theorem nat.prime.not_dvd_one {p : } :
¬p 1

theorem nat.not_prime_mul {a b : } :
1 < a1 < b¬nat.prime (a * b)

def nat.min_fac_aux  :

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
def nat.min_fac  :

Returns the smallest prime factor of n ≠ 1.

Equations
@[simp]
theorem nat.min_fac_zero  :

@[simp]
theorem nat.min_fac_one  :

theorem nat.min_fac_eq (n : ) :
n.min_fac = ite (2 n) 2 (n.min_fac_aux 3)

theorem nat.min_fac_aux_has_prop {n : } (n2 : 2 n) (nd2 : ¬2 n) (k i : ) :
k = 2 * i + 3(∀ (m : ), 2 mm nk m)min_fac_prop n (n.min_fac_aux k)

theorem nat.min_fac_has_prop {n : } :
n 1min_fac_prop n n.min_fac

theorem nat.min_fac_dvd (n : ) :

theorem nat.min_fac_prime {n : } :
n 1

theorem nat.min_fac_le_of_dvd {n m : } :
2 mm nn.min_fac m

theorem nat.min_fac_pos (n : ) :

theorem nat.min_fac_le {n : } :
0 < nn.min_fac n

theorem nat.prime_def_min_fac {p : } :
2 p p.min_fac = p

@[instance]
def nat.decidable_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
theorem nat.not_prime_iff_min_fac_lt {n : } :
2 n(¬ n.min_fac < n)

theorem nat.min_fac_le_div {n : } :
0 < nn.min_fac n / n.min_fac

theorem nat.min_fac_sq_le_self {n : } :
0 < nn.min_fac ^ 2 n

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

@[simp]
theorem nat.min_fac_eq_one_iff {n : } :
n.min_fac = 1 n = 1

@[simp]
theorem nat.min_fac_eq_two_iff (n : ) :
n.min_fac = 2 2 n

theorem nat.exists_dvd_of_not_prime {n : } :
2 n(∃ (m : ), m n m 1 m n)

theorem nat.exists_dvd_of_not_prime2 {n : } :
2 n(∃ (m : ), m n 2 m m < n)

theorem nat.exists_prime_and_dvd {n : } :
2 n(∃ (p : ), p n)

theorem nat.exists_infinite_primes (n : ) :
∃ (p : ), n 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.

theorem nat.prime.eq_two_or_odd {p : } :
p = 2 p % 2 = 1

theorem nat.coprime_of_dvd {m n : } :
(∀ (k : ), k m¬k n)m.coprime n

theorem nat.coprime_of_dvd' {m n : } :
(∀ (k : ), k mk nk 1)m.coprime n

theorem nat.factors_lemma {k : } :
(k + 2) / (k + 2).min_fac < k + 2

def nat.factors  :

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

Equations
theorem nat.mem_factors {n p : } :
p n.factors

theorem nat.prod_factors {n : } :
0 < nn.factors.prod = n

theorem nat.factors_prime {p : } :
p.factors = [p]

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.

theorem nat.prime.coprime_iff_not_dvd {p n : } :
(p.coprime n ¬p n)

theorem nat.prime.dvd_iff_not_coprime {p n : } :
(p n ¬p.coprime n)

theorem nat.prime.not_coprime_iff_dvd {m n : } :
¬m.coprime n ∃ (p : ), p m p n

theorem nat.prime.dvd_mul {p m n : } :
(p m * n p m p n)

theorem nat.prime.not_dvd_mul {p m n : } :
¬p m¬p n¬p m * n

theorem nat.prime.dvd_of_dvd_pow {p m n : } :
p m ^ np m

theorem nat.prime.pow_not_prime {x n : } :
2 n¬nat.prime (x ^ n)

theorem nat.prime.mul_eq_prime_pow_two_iff {x y p : } :
x 1y 1(x * y = p ^ 2 x = p y = p)

theorem nat.prime.dvd_factorial {n p : } :
(p n! p n)

theorem nat.prime.coprime_pow_of_not_dvd {p m a : } :
¬p aa.coprime (p ^ m)

theorem nat.coprime_primes {p q : } :
(p.coprime q p q)

theorem nat.coprime_pow_primes {p q : } (n m : ) :
p q(p ^ n).coprime (q ^ m)

theorem nat.coprime_or_dvd_of_prime {p : } (pp : nat.prime p) (i : ) :
p.coprime i p i

theorem nat.dvd_prime_pow {p : } (pp : nat.prime p) {m i : } :
i p ^ m ∃ (k : ) (H : k m), i = p ^ k

theorem nat.eq_prime_pow_of_dvd_least_prime_pow {a p k : } :
¬a p ^ ka 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).

theorem nat.mem_list_primes_of_dvd_prod {p : } (hp : nat.prime p) {l : list } :
(∀ (p : ), p lp l.prodp l

theorem nat.mem_factors_iff_dvd {n p : } :
0 < n(p n.factors p n)

theorem nat.perm_of_prod_eq_prod {l₁ l₂ : list } :
l₁.prod = l₂.prod(∀ (p : ), p l₁(∀ (p : ), p l₂l₁ ~ l₂

theorem nat.factors_unique {n : } {l : list } :
l.prod = n(∀ (p : ), p ll ~ n.factors

theorem nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (p_prime : nat.prime p) {m n k l : } :
p ^ k mp ^ l np ^ (k + l + 1) m * np ^ (k + 1) m p ^ (l + 1) n

def nat.primes  :
Type

The type of prime numbers

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
theorem nat.primes.coe_nat_inj (p q : nat.primes) :
p = qp = q

@[instance]
def nat.monoid.prime_pow {α : Type u_1} [monoid α] :

Equations