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.

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)

Equations

• ⋯ = ⋯

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 ∣ p → m = 1 ∨ m = p

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

def Nat.decidablePrime1 (p : ℕ) : Decidable (Nat.Prime p)

This instance is slower than the instance decidablePrime 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 by decide, but rather by norm_num, which is much faster.

Equations

• p.decidablePrime1 = 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

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

This instance is faster in the virtual machine than decidablePrime1, but slower in the kernel.

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 ∧ p.minFac = p) ⋯

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.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 : Nat.Primes) (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)

Equations

• Nat.fact_prime_two = ⋯

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

Equations

• Nat.fact_prime_three = ⋯