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 ↔ Nat.Prime a

theorem Nat.not_prime_zero : ¬Nat.Prime 0

theorem Nat.not_prime_one : ¬Nat.Prime 1

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 p → 2 ≤ p

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

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

instance 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 {p : ℕ} : Nat.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.

@[deprecated Nat.prime_def]

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

Alias of Nat.prime_def.

---

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 : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1

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

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

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

instance Nat.decidablePrime (p : ℕ) : Decidable (Nat.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) ⋯

theorem Nat.prime_two : Nat.Prime 2

theorem Nat.prime_three : Nat.Prime 3

theorem Nat.prime_five : Nat.Prime 5

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.minFac_lemma (n k : ℕ) (h : ¬n < k * k) : n.sqrt - k < n.sqrt + 2 - k

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.

By default this well-founded recursion would be irreducible. This prevents use decide to resolve Nat.prime n for small values of n, so we mark this as @[semireducible].

In future, we may want to remove this annotation and instead use norm_num instead of decide in these situations.

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 : Nat.minFac 0 = 2

@[simp]

theorem Nat.minFac_one : Nat.minFac 1 = 1

@[simp]

theorem Nat.minFac_two : Nat.minFac 2 = 2

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

@[irreducible]

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) : Nat.Prime n.minFac

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 : ℕ), Nat.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 : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ p.minFac = p

@[simp]

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

def Nat.decidablePrime' (p : ℕ) : Decidable (Nat.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 : Nat.decidablePrime = Nat.decidablePrime'

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

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

theorem Nat.minFac_sq_le_self {n : ℕ} (w : 0 < n) (h : ¬Nat.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 : ℕ), Nat.Prime p ∧ p ∣ n

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

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

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

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

theorem Nat.Prime.prime {p : ℕ} : Nat.Prime p → 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.

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

def Nat.Primes : Type

The type of prime numbers

Equations

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

instance Nat.instPrimesDecidableEq : DecidableEq Nat.Primes

Equations

• Nat.instPrimesDecidableEq a b = a.instDecidableEq b

instance Nat.Primes.instRepr : Repr Nat.Primes

Equations

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

instance Nat.Primes.inhabitedPrimes : Inhabited Nat.Primes

Equations

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

instance Nat.Primes.coeNat : Coe Nat.Primes ℕ

Equations

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

theorem Nat.Primes.coe_nat_injective : Function.Injective fun (a : Nat.Primes) => ↑a

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

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

Equations

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

instance Nat.fact_prime_two : Fact (Nat.Prime 2)

instance Nat.fact_prime_three : Fact (Nat.Prime 3)