Prime numbers

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

Important declarations

• Nat.Prime: the predicate that expresses that a natural number p is prime
• Nat.Primes: the subtype of natural numbers that are prime
• Nat.minFac n: the minimal prime factor of a natural number n ≠ 1
• Nat.prime_iff: Nat.Prime coincides with the general definition of Prime
• Nat.irreducible_iff_nat_prime: a non-unit natural number is only divisible by 1 iff it is prime

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. The theorem Nat.prime_def witnesses this description of a prime number.

Equations

• Nat.Prime p = Irreducible p

theorem Nat.irreducible_iff_nat_prime (a : ℕ) : Irreducible a ↔ Prime a

theorem Nat.not_prime_zero : ¬Prime 0

theorem Nat.prime_zero_false : Prime 0 → False

A copy of not_prime_zero stated in a way that works for aesop.

See https://github.com/leanprover-community/aesop/issues/197 for an explanation.

theorem Nat.not_prime_one : ¬Prime 1

theorem Nat.prime_one_false : Prime 1 → False

A copy of not_prime_one stated in a way that works for aesop.

See https://github.com/leanprover-community/aesop/issues/197 for an explanation.

theorem Nat.Prime.ne_zero {n : ℕ} (h : Prime n) : n ≠ 0

theorem Nat.Prime.pos {p : ℕ} (pp : Prime p) : 0 < p

theorem Nat.Prime.two_le {p : ℕ} : Prime p → 2 ≤ p

theorem Nat.Prime.one_lt {p : ℕ} : Prime p → 1 < p

theorem Nat.Prime.one_le {p : ℕ} (hp : Prime p) : 1 ≤ p

instance Nat.Prime.one_lt' (p : ℕ) [hp : Fact (Prime p)] : Fact (1 < p)

theorem Nat.Prime.ne_one {p : ℕ} (hp : Prime p) : p ≠ 1

theorem Nat.Prime.eq_one_or_self_of_dvd {p : ℕ} (pp : Prime p) (m : ℕ) (hm : m ∣ p) : m = 1 ∨ m = p

theorem Nat.prime_def {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

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. The theorem Nat.prime_def witnesses this description of a prime number.

theorem Nat.prime_def_lt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1

theorem Nat.prime_def_lt' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p

theorem Nat.prime_def_le_sqrt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p

theorem Nat.prime_iff_not_exists_mul_eq {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ¬∃ (m : ℕ), ∃ (n : ℕ), m < p ∧ n < p ∧ m * n = p

theorem Nat.prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m) : Prime n

@[instance_reducible]

instance Nat.decidablePrime (p : ℕ) : Decidable (Prime p)

This instance is set up to work in the kernel (by decide) for small values.

Below (decidablePrime') we will define a faster variant to be used by the compiler (e.g. in #eval or by native_decide).

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

Equations

• p.decidablePrime = decidable_of_iff' (2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) ⋯

Specific small primes

It is recommended not to add further lemmas to this list; instead, import Mathlib.Tactic.NormNum.Prime in downstream files and use norm_num for primality proofs.

theorem Nat.prime_two : Prime 2

theorem Nat.prime_three : Prime 3

theorem Nat.prime_five : Prime 5

theorem Nat.prime_seven : Prime 7

theorem Nat.prime_eleven : Prime 11

theorem Nat.dvd_prime {p m : ℕ} (pp : Prime p) : m ∣ p ↔ m = 1 ∨ m = p

theorem Nat.dvd_prime_two_le {p m : ℕ} (pp : Prime p) (H : 2 ≤ m) : m ∣ p ↔ m = p

theorem Nat.prime_dvd_prime_iff_eq {p q : ℕ} (pp : Prime p) (qp : Prime q) : p ∣ q ↔ p = q

theorem Nat.Prime.not_dvd_one {p : ℕ} (pp : Prime p) : ¬p ∣ 1

theorem Nat.minFac_lemma (n k : ℕ) (h : ¬n < k * k) : n.sqrt - k < n.sqrt + 2 - k

@[irreducible]

def Nat.minFacAux (n : ℕ) : ℕ → ℕ

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

This definition is by well-founded recursion, so rfl or decide cannot be used. One can use norm_num to prove Nat.prime n for small n.

Equations

• n.minFacAux x✝ = if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2)

def Nat.minFac (n : ℕ) : ℕ

Returns the smallest prime factor of n ≠ 1.

Equations

• n.minFac = if 2 ∣ n then 2 else n.minFacAux 3

@[simp]

theorem Nat.minFac_zero : minFac 0 = 2

@[simp]

theorem Nat.minFac_one : minFac 1 = 1

@[simp]

theorem Nat.minFac_two : minFac 2 = 2

theorem Nat.minFac_eq (n : ℕ) : n.minFac = if 2 ∣ n then 2 else n.minFacAux 3

theorem Nat.minFacAux_has_prop {n : ℕ} (n2 : 2 ≤ n) (k i : ℕ) : k = 2 * i + 3 → (∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m) → Nat.minFacProp✝ n (n.minFacAux k)

theorem Nat.minFac_has_prop {n : ℕ} (n1 : n ≠ 1) : Nat.minFacProp✝ n n.minFac

theorem Nat.minFac_dvd (n : ℕ) : n.minFac ∣ n

theorem Nat.minFac_prime {n : ℕ} (n1 : n ≠ 1) : Prime n.minFac

@[simp]

theorem Nat.minFac_prime_iff {n : ℕ} : Prime n.minFac ↔ n ≠ 1

theorem Nat.minFac_le_of_dvd {n m : ℕ} : 2 ≤ m → m ∣ n → n.minFac ≤ m

theorem Nat.minFac_pos (n : ℕ) : 0 < n.minFac

theorem Nat.minFac_le {n : ℕ} (H : 0 < n) : n.minFac ≤ n

theorem Nat.le_minFac {m n : ℕ} : n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), Prime p → p ∣ n → m ≤ p

theorem Nat.le_minFac' {m n : ℕ} : n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), 2 ≤ p → p ∣ n → m ≤ p

theorem Nat.prime_def_minFac {p : ℕ} : Prime p ↔ 2 ≤ p ∧ p.minFac = p

@[simp]

theorem Nat.Prime.minFac_eq {p : ℕ} (hp : Prime p) : p.minFac = p

def Nat.decidablePrime' (p : ℕ) : Decidable (Prime p)

This definition is faster in the virtual machine than decidablePrime, but slower in the kernel.

Equations

• p.decidablePrime' = decidable_of_iff' (2 ≤ p ∧ p.minFac = p) ⋯

@[csimp]

theorem Nat.decidablePrime_csimp : decidablePrime = decidablePrime'

theorem Nat.not_prime_iff_minFac_lt {n : ℕ} (n2 : 2 ≤ n) : ¬Prime n ↔ n.minFac < n

theorem Nat.minFac_le_div {n : ℕ} (pos : 0 < n) (np : ¬Prime n) : n.minFac ≤ n / n.minFac

theorem Nat.minFac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬Prime n) : n.minFac ^ 2 ≤ n

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

@[simp]

theorem Nat.minFac_eq_one_iff {n : ℕ} : n.minFac = 1 ↔ n = 1

@[simp]

theorem Nat.minFac_eq_two_iff (n : ℕ) : n.minFac = 2 ↔ 2 ∣ n

theorem Nat.factors_lemma {k : ℕ} : (k + 2) / (k + 2).minFac < k + 2

theorem Nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ (p : ℕ), Prime p ∧ p ∣ n

theorem Nat.coprime_of_dvd {m n : ℕ} (H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n) : m.Coprime n

theorem Nat.Prime.coprime_iff_not_dvd {p n : ℕ} (pp : Prime p) : p.Coprime n ↔ ¬p ∣ n

theorem Nat.Prime.dvd_mul {p m n : ℕ} (pp : Prime p) : p ∣ m * n ↔ p ∣ m ∨ p ∣ n

theorem Nat.Prime.dvd_or_dvd {p m n : ℕ} (pp : Prime p) : p ∣ m * n → p ∣ m ∨ p ∣ n

Alias of the forward direction of Nat.Prime.dvd_mul.

theorem Nat.prime_iff {p : ℕ} : Prime p ↔ _root_.Prime p

theorem Nat.Prime.prime {p : ℕ} : Prime p → _root_.Prime p

Alias of the forward direction of Nat.prime_iff.

theorem Prime.nat_prime {p : ℕ} : Prime p → Nat.Prime p

Alias of the reverse direction of Nat.prime_iff.

@[instance_reducible]

instance Nat.instDecidablePredPrime : DecidablePred _root_.Prime

Equations

• n.instDecidablePredPrime = decidable_of_iff (Nat.Prime n) ⋯

theorem Nat.irreducible_iff_prime {p : ℕ} : Irreducible p ↔ _root_.Prime p

@[instance_reducible]

instance Nat.instDecidablePredIrreducible : DecidablePred Irreducible

Equations

• Nat.instDecidablePredIrreducible = Nat.decidablePrime

def Nat.Primes : Type

The type of prime numbers

Equations

• Nat.Primes = { p : ℕ // Nat.Prime p }

@[instance_reducible]

instance Nat.instDecidableEqPrimes : DecidableEq Primes

Equations

• Nat.instDecidableEqPrimes = Nat.instDecidableEqPrimes._aux_1

@[instance_reducible]

instance Nat.Primes.instRepr : Repr Primes

Equations

• Nat.Primes.instRepr = { reprPrec := fun (p : Nat.Primes) (x : ℕ) => repr ↑p }

@[instance_reducible]

instance Nat.Primes.inhabitedPrimes : Inhabited Primes

Equations

• Nat.Primes.inhabitedPrimes = { default := ⟨2, Nat.prime_two⟩ }

@[instance_reducible]

instance Nat.Primes.coeNat : Coe Primes ℕ

Equations

• Nat.Primes.coeNat = { coe := Subtype.val }

theorem Nat.Primes.coe_nat_injective : Function.Injective Subtype.val

theorem Nat.Primes.coe_nat_inj (p q : Primes) : ↑p = ↑q ↔ p = q

@[instance_reducible]

instance Nat.monoid.primePow {α : Type u_1} [Monoid α] : Pow α Primes

Equations

• Nat.monoid.primePow = { pow := fun (x : α) (p : Nat.Primes) => x ^ ↑p }

instance Nat.fact_prime_two : Fact (Prime 2)

instance Nat.fact_prime_three : Fact (Prime 3)