mathlib documentation

data.nat.prime

Prime numbers #

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

Important declarations #

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
Instances for nat.prime
theorem nat.prime.ne_zero {n : } (h : nat.prime n) :
n 0
theorem nat.prime.pos {p : } (pp : nat.prime p) :
0 < p
theorem nat.prime.two_le {p : } :
nat.prime p2 p
theorem nat.prime.one_lt {p : } :
nat.prime p1 < p
@[protected, instance]
def nat.prime.one_lt' (p : ) [hp : fact (nat.prime p)] :
fact (1 < p)
theorem nat.prime.ne_one {p : } (hp : nat.prime p) :
p 1
theorem nat.prime.eq_one_or_self_of_dvd {p : } (pp : nat.prime p) (m : ) (hm : m p) :
m = 1 m = p
theorem nat.prime_def_lt'' {p : } :
nat.prime p 2 p ∀ (m : ), m pm = 1 m = p
theorem nat.prime_def_lt {p : } :
nat.prime p 2 p ∀ (m : ), m < pm pm = 1
theorem nat.prime_def_lt' {p : } :
nat.prime p 2 p ∀ (m : ), 2 mm < p¬m p
theorem nat.prime_def_le_sqrt {p : } :
nat.prime p 2 p ∀ (m : ), 2 mm nat.sqrt p¬m p
theorem nat.prime_of_coprime (n : ) (h1 : 1 < n) (h : ∀ (m : ), m < nm 0n.coprime m) :

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
theorem nat.prime.pred_pos {p : } (pp : nat.prime p) :
0 < p.pred
theorem nat.succ_pred_prime {p : } (pp : nat.prime p) :
p.pred.succ = p
theorem nat.dvd_prime {p m : } (pp : nat.prime p) :
m p m = 1 m = p
theorem nat.dvd_prime_two_le {p m : } (pp : nat.prime p) (H : 2 m) :
m p m = p
theorem nat.prime_dvd_prime_iff_eq {p q : } (pp : nat.prime p) (qp : nat.prime q) :
p q p = q
theorem nat.prime.not_dvd_one {p : } (pp : nat.prime p) :
¬p 1
theorem nat.not_prime_mul {a b : } (a1 : 1 < a) (b1 : 1 < b) :
theorem nat.not_prime_mul' {a b n : } (h : a * b = n) (h₁ : 1 < a) (h₂ : 1 < b) :
theorem nat.prime_mul_iff {a b : } :
theorem nat.prime.dvd_iff_eq {p a : } (hp : nat.prime p) (a1 : a 1) :
a p p = a
theorem nat.min_fac_lemma (n k : ) (h : ¬n < k * k) :
nat.sqrt n - k < nat.sqrt n + 2 - k
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
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) (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 : } (n1 : n 1) :
min_fac_prop n n.min_fac
theorem nat.min_fac_dvd (n : ) :
theorem nat.min_fac_prime {n : } (n1 : 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 : } (H : 0 < n) :
theorem nat.le_min_fac {m n : } :
n = 1 m n.min_fac ∀ (p : ), nat.prime pp nm p
theorem nat.le_min_fac' {m n : } :
n = 1 m n.min_fac ∀ (p : ), 2 pp nm p
@[simp]
theorem nat.prime.min_fac_eq {p : } (hp : nat.prime p) :
@[protected, instance]

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 : } (n2 : 2 n) :
theorem nat.min_fac_le_div {n : } (pos : 0 < n) (np : ¬nat.prime n) :
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.

@[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 : } (n2 : 2 n) (np : ¬nat.prime n) :
∃ (m : ), m n m 1 m n
theorem nat.exists_dvd_of_not_prime2 {n : } (n2 : 2 n) (np : ¬nat.prime n) :
∃ (m : ), m n 2 m m < n
theorem nat.exists_prime_and_dvd {n : } (hn : n 1) :
∃ (p : ), nat.prime p p n
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.

A version of nat.exists_infinite_primes using the bdd_above predicate.

A version of nat.exists_infinite_primes using the set.infinite predicate.

theorem nat.prime.eq_two_or_odd {p : } (hp : nat.prime p) :
p = 2 p % 2 = 1
theorem nat.prime.eq_two_or_odd' {p : } (hp : nat.prime p) :
p = 2 odd p
theorem nat.prime.even_iff {p : } (hp : nat.prime p) :
even p p = 2
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.

theorem nat.coprime_of_dvd {m n : } (H : ∀ (k : ), nat.prime kk m¬k n) :
theorem nat.coprime_of_dvd' {m n : } (H : ∀ (k : ), nat.prime kk mk nk 1) :
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
@[simp]
@[simp]
theorem nat.prime_of_mem_factors {n p : } :
theorem nat.pos_of_mem_factors {n p : } (h : p n.factors) :
0 < p
theorem nat.prod_factors {n : } :
n 0n.factors.prod = n
theorem nat.factors_prime {p : } (hp : nat.prime p) :
p.factors = [p]
theorem nat.factors_chain {n a : } :
(∀ (p : ), nat.prime pp na p)list.chain has_le.le a n.factors
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.

@[simp]
theorem nat.factors_eq_nil (n : ) :
n.factors = list.nil n = 0 n = 1
theorem nat.eq_of_perm_factors {a b : } (ha : a 0) (hb : b 0) (h : a.factors ~ b.factors) :
a = b
theorem nat.prime.coprime_iff_not_dvd {p n : } (pp : nat.prime p) :
p.coprime n ¬p n
theorem nat.prime.dvd_iff_not_coprime {p n : } (pp : nat.prime p) :
p n ¬p.coprime n
theorem nat.prime.not_coprime_iff_dvd {m n : } :
¬m.coprime n ∃ (p : ), nat.prime p p m p n
theorem nat.prime.dvd_mul {p m n : } (pp : nat.prime p) :
p m * n p m p n
theorem nat.prime.not_dvd_mul {p m n : } (pp : nat.prime p) (Hm : ¬p m) (Hn : ¬p n) :
¬p m * n
theorem nat.prime_iff {p : } :
theorem nat.prime.dvd_of_dvd_pow {p m n : } (pp : nat.prime p) (h : p m ^ n) :
p m
theorem nat.prime.pow_not_prime {x n : } (hn : 2 n) :
theorem nat.prime.pow_not_prime' {x n : } :
n 1¬nat.prime (x ^ n)
theorem nat.prime.eq_one_of_pow {x n : } (h : nat.prime (x ^ n)) :
n = 1
theorem nat.prime.pow_eq_iff {p a k : } (hp : nat.prime p) :
a ^ k = p a = p k = 1
theorem nat.pow_min_fac {n k : } (hk : k 0) :
(n ^ k).min_fac = n.min_fac
theorem nat.prime.pow_min_fac {p k : } (hp : nat.prime p) (hk : k 0) :
(p ^ k).min_fac = p
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
theorem nat.prime.dvd_factorial {n p : } (hp : nat.prime p) :
theorem nat.prime.coprime_pow_of_not_dvd {p m a : } (pp : nat.prime p) (h : ¬p a) :
a.coprime (p ^ m)
theorem nat.coprime_primes {p q : } (pp : nat.prime p) (pq : nat.prime q) :
p.coprime q p q
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)
theorem nat.coprime_or_dvd_of_prime {p : } (pp : nat.prime p) (i : ) :
p.coprime i p i
theorem nat.coprime_of_lt_prime {n p : } (n_pos : 0 < n) (hlt : n < p) (pp : nat.prime p) :
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
theorem nat.dvd_prime_pow {p : } (pp : nat.prime p) {m i : } :
i p ^ m ∃ (k : ) (H : k m), i = p ^ k
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
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).

theorem nat.ne_one_iff_exists_prime_dvd {n : } :
n 1 ∃ (p : ), nat.prime p p n
theorem nat.eq_one_iff_not_exists_prime_dvd {n : } :
n = 1 ∀ (p : ), nat.prime p¬p n
theorem nat.mem_factors_iff_dvd {n p : } (hn : n 0) (hp : nat.prime p) :
p n.factors p n
theorem nat.dvd_of_mem_factors {n p : } (h : p n.factors) :
p n
theorem nat.mem_factors {n p : } (hn : n 0) :
theorem nat.le_of_mem_factors {n p : } (h : p n.factors) :
p n
theorem nat.factors_unique {n : } {l : list } (h₁ : l.prod = n) (h₂ : ∀ (p : ), p lnat.prime p) :

Fundamental theorem of arithmetic

theorem nat.prime.factors_pow {p : } (hp : nat.prime p) (n : ) :
theorem nat.eq_prime_pow_of_unique_prime_dvd {n p : } (hpos : n 0) (h : ∀ {d : }, nat.prime dd nd = p) :
theorem nat.perm_factors_mul {a b : } (ha : a 0) (hb : b 0) :

For positive a and b, the prime factors of a * b are the union of those of a and b

theorem nat.perm_factors_mul_of_coprime {a b : } (hab : a.coprime b) :

For coprime a and b, the prime factors of a * b are the union of those of a and b

theorem nat.factors_sublist_right {n k : } (h : k 0) :
theorem nat.factors_sublist_of_dvd {n k : } (h : n k) (h' : k 0) :
theorem nat.factors_subset_right {n k : } (h : k 0) :
theorem nat.factors_subset_of_dvd {n k : } (h : n k) (h' : k 0) :
theorem nat.dvd_of_factors_subperm {a b : } (ha : a 0) (h : a.factors <+~ b.factors) :
a b
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
def nat.primes  :
Type

The type of prime numbers

Equations
Instances for nat.primes
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem nat.primes.coe_nat_inj (p q : nat.primes) :
p = qp = q
@[protected, instance]
def nat.monoid.prime_pow {α : Type u_1} [monoid α] :
Equations

Primality prover #

theorem tactic.norm_num.is_prime_helper (n : ) (h₁ : 1 < n) (h₂ : n.min_fac = n) :
def tactic.norm_num.min_fac_helper (n k : ) :
Prop

A predicate representing partial progress in a proof of min_fac.

Equations
theorem tactic.norm_num.min_fac_helper_3 (n k k' c : ) (e : k + 1 = k') (nc : bit1 n % bit1 k = c) (c0 : 0 < c) (h : tactic.norm_num.min_fac_helper n k) :
theorem tactic.norm_num.min_fac_helper_5 (n k k' : ) (e : bit1 k * bit1 k = k') (hd : bit1 n < k') (h : tactic.norm_num.min_fac_helper n k) :
meta def tactic.norm_num.prove_non_prime (e : expr) (n d₁ : ) :

Given e a natural numeral and d : nat a factor of it, return ⊢ ¬ prime e.

Given a,a1 := bit1 a, n1 the value of a1, b and p : min_fac_helper a b, returns (c, ⊢ min_fac a1 = c).

Given a a natural numeral, returns (b, ⊢ min_fac a = b).

def tactic.norm_num.factors_helper (n p : ) (l : list ) :
Prop

A partial proof of factors. Asserts that l is a sorted list of primes, lower bounded by a prime p, which multiplies to n.

Equations
theorem tactic.norm_num.factors_helper_cons' (n m a b : ) (l : list ) (h₁ : b * m = n) (h₂ : a b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
theorem tactic.norm_num.factors_helper_cons (n m a b : ) (l : list ) (h₁ : b * m = n) (h₂ : a < b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
theorem tactic.norm_num.factors_helper_sn (n a : ) (h₁ : a < n) (h₂ : n.min_fac = n) :

Given n and a natural numerals, returns (l, ⊢ factors_helper n a l).

Evaluates the prime and min_fac functions.

@[protected, instance]
@[protected, instance]
theorem nat.mem_factors_mul {a b : } (ha : a 0) (hb : b 0) {p : } :
theorem nat.factors_mul_to_finset {a b : } (ha : a 0) (hb : b 0) :

If a, b are positive, the prime divisors of a * b are the union of those of a and b

theorem nat.pow_factors_to_finset (n : ) {k : } (hk : k 0) :
theorem nat.prime_pow_prime_divisor {p k : } (hk : k 0) (hp : nat.prime p) :
(p ^ k).factors.to_finset = {p}

The only prime divisor of positive prime power p^k is p itself

theorem nat.coprime_factors_disjoint {a b : } (hab : a.coprime b) :

The sets of factors of coprime a and b are disjoint

theorem nat.mem_factors_mul_of_coprime {a b : } (hab : a.coprime b) (p : ) :
theorem nat.mem_factors_mul_left {p a b : } (hpa : p a.factors) (hb : b 0) :
p (a * b).factors

If p is a prime factor of a then p is also a prime factor of a * b for any b > 0

theorem nat.mem_factors_mul_right {p a b : } (hpb : p b.factors) (ha : a 0) :
p (a * b).factors

If p is a prime factor of b then p is also a prime factor of a * b for any a > 0

theorem nat.eq_two_pow_or_exists_odd_prime_and_dvd (n : ) :
(∃ (k : ), n = 2 ^ k) ∃ (p : ), nat.prime p p n odd p
theorem int.prime_two  :
theorem int.prime_three  :
theorem card_multiples (n p : ) :
(finset.filter (λ (e : ), p e + 1) (finset.range n)).card = n / p

Exactly n / p naturals in [1, n] are multiples of p.