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.exists_infinite_primes: Euclid's theorem that there exist infinitely many prime numbers. This also appears as Nat.not_bddAbove_setOf_prime and Nat.infinite_setOf_prime (the latter in Data.Nat.PrimeFin).
• 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 < 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 < 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.Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p

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.prime_mul_iff {a : ℕ} {b : ℕ} : Nat.Prime (a * b) ↔ Nat.Prime a ∧ b = 1 ∨ Nat.Prime b ∧ a = 1

theorem Nat.not_prime_mul {a : ℕ} {b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Nat.Prime (a * b)

theorem Nat.not_prime_mul' {a : ℕ} {b : ℕ} {n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Nat.Prime n

theorem Nat.Prime.dvd_iff_eq {p : ℕ} {a : ℕ} (hp : Nat.Prime p) (a1 : a ≠ 1) : a ∣ p ↔ p = a

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.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.not_prime_of_dvd_of_ne {m : ℕ} {n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Nat.Prime n

theorem Nat.not_prime_of_dvd_of_lt {m : ℕ} {n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Nat.Prime n

theorem Nat.not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

theorem Nat.not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : ¬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.dvd_of_forall_prime_mul_dvd {a : ℕ} {b : ℕ} (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ a → p * a ∣ b) : a ∣ b

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.

theorem Nat.not_bddAbove_setOf_prime : ¬BddAbove {p : ℕ | Nat.Prime p}

A version of Nat.exists_infinite_primes using the BddAbove 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.odd_of_ne_two {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) : Odd p

theorem Nat.Prime.even_sub_one {p : ℕ} (hp : Nat.Prime p) (h2 : p ≠ 2) : Even (p - 1)

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 k → k ∣ m → ¬k ∣ n) : m.Coprime n

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

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

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

@[simp]

theorem Nat.coprime_two_left {n : ℕ} : Nat.Coprime 2 n ↔ Odd n

@[simp]

theorem Nat.coprime_two_right {n : ℕ} : n.Coprime 2 ↔ Odd n

theorem Nat.Coprime.odd_of_left {n : ℕ} : Nat.Coprime 2 n → Odd n

Alias of the forward direction of Nat.coprime_two_left.

theorem Odd.coprime_two_left {n : ℕ} : Odd n → Nat.Coprime 2 n

Alias of the reverse direction of Nat.coprime_two_left.

theorem Odd.coprime_two_right {n : ℕ} : Odd n → n.Coprime 2

Alias of the reverse direction of Nat.coprime_two_right.

theorem Nat.Coprime.odd_of_right {n : ℕ} : n.Coprime 2 → Odd n

Alias of the forward direction of Nat.coprime_two_right.

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

theorem Nat.Prime.dvd_of_dvd_pow {p : ℕ} {m : ℕ} {n : ℕ} (pp : Nat.Prime p) (h : p ∣ m ^ n) : p ∣ m

theorem Nat.Prime.not_prime_pow' {x : ℕ} {n : ℕ} (hn : n ≠ 1) : ¬Nat.Prime (x ^ n)

theorem Nat.Prime.not_prime_pow {x : ℕ} {n : ℕ} (hn : 2 ≤ n) : ¬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_minFac {n : ℕ} {k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac

theorem Nat.Prime.pow_minFac {p : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : (p ^ k).minFac = 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 : ℕ} : Nat.Prime p → (p ∣ n.factorial ↔ p ≤ n)

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) : p.Coprime n

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 ≤ 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.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

theorem Nat.prime_iff_prime_int {p : ℕ} : Nat.Prime p ↔ Prime ↑p

theorem Nat.Prime.pow_inj {p : ℕ} {q : ℕ} {m : ℕ} {n : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n

Two prime powers with positive exponents are equal only when the primes and the exponents are equal.

theorem Nat.exists_pow_lt_factorial (c : ℕ) : ∃ n0 > 1, ∀ n ≥ n0, c ^ n < (n - 1).factorial

theorem Nat.exists_mul_pow_lt_factorial (a : ℕ) (c : ℕ) : ∃ (n0 : ℕ), ∀ n ≥ n0, a * c ^ n < (n - 1).factorial

theorem Nat.exists_prime_mul_pow_lt_factorial (n : ℕ) (a : ℕ) (c : ℕ) : ∃ p > n, Nat.Prime p ∧ a * c ^ p < (p - 1).factorial

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 = ⋯

theorem Int.prime_two : Prime 2

theorem Int.prime_three : Prime 3