Fermat Pseudoprimes

In this file we define Fermat pseudoprimes: composite numbers that pass the Fermat primality test. A natural number n passes the Fermat primality test to base b (and is therefore deemed a "probable prime") if n divides b ^ (n - 1) - 1. n is a Fermat pseudoprime to base b if n is a composite number that passes the Fermat primality test to base b and is coprime with b.

Fermat pseudoprimes can also be seen as composite numbers for which Fermat's little theorem holds true.

Numbers which are Fermat pseudoprimes to all bases are known as Carmichael numbers (not yet defined in this file).

Main Results

The main definitions for this file are

• Nat.ProbablePrime: A number n is a probable prime to base b if it passes the Fermat primality test; that is, if n divides b ^ (n - 1) - 1
• Nat.FermatPsp: A number n is a pseudoprime to base b if it is a probable prime to base b, is composite, and is coprime with b (this last condition is automatically true if n divides b ^ (n - 1) - 1, but some sources include it in the definition).

Note that all composite numbers are pseudoprimes to base 0 and 1, and that the definition of Nat.ProbablePrime in this file implies that all numbers are probable primes to bases 0 and 1, and that 0 and 1 are probable primes to any base.

The main theorems are

• Nat.exists_infinite_pseudoprimes: there are infinite pseudoprimes to any base b ≥ 1

def Nat.ProbablePrime (n b : ℕ) : Prop

n is a probable prime to base b if n passes the Fermat primality test; that is, n divides b ^ (n - 1) - 1. This definition implies that all numbers are probable primes to base 0 or 1, and that 0 and 1 are probable primes to any base.

Equations

• n.ProbablePrime b = (n ∣ b ^ (n - 1) - 1)

def Nat.FermatPsp (n b : ℕ) : Prop

n is a Fermat pseudoprime to base b if n is a probable prime to base b and is composite. By this definition, all composite natural numbers are pseudoprimes to base 0 and 1. This definition also permits n to be less than b, so that 4 is a pseudoprime to base 5, for example.

Equations

• n.FermatPsp b = (n.ProbablePrime b ∧ ¬Nat.Prime n ∧ 1 < n)

instance Nat.decidableProbablePrime (n b : ℕ) : Decidable (n.ProbablePrime b)

Equations

• n.decidableProbablePrime b = n.decidable_dvd (b ^ (n - 1) - 1)

instance Nat.decidablePsp (n b : ℕ) : Decidable (n.FermatPsp b)

Equations

• n.decidablePsp b = inferInstanceAs (Decidable (n.ProbablePrime b ∧ ¬Nat.Prime n ∧ 1 < n))

theorem Nat.coprime_of_probablePrime {n b : ℕ} (h : n.ProbablePrime b) (h₁ : 1 ≤ n) (h₂ : 1 ≤ b) : n.Coprime b

If n passes the Fermat primality test to base b, then n is coprime with b, assuming that n and b are both positive.

theorem Nat.probablePrime_iff_modEq (n : ℕ) {b : ℕ} (h : 1 ≤ b) : n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

theorem Nat.coprime_of_fermatPsp {n b : ℕ} (h : n.FermatPsp b) (h₁ : 1 ≤ b) : n.Coprime b

If n is a Fermat pseudoprime to base b, then n is coprime with b, assuming that b is positive.

This lemma is a small wrapper based on coprime_of_probablePrime

theorem Nat.fermatPsp_base_one {n : ℕ} (h₁ : 1 < n) (h₂ : ¬Nat.Prime n) : n.FermatPsp 1

All composite numbers are Fermat pseudoprimes to base 1.

theorem Nat.exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) : ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n

For all positive bases, there exist infinite Fermat pseudoprimes to that base. Given in this form: for all numbers b ≥ 1 and m, there exists a pseudoprime n to base b such that m ≤ n. This form is similar to Nat.exists_infinite_primes.

theorem Nat.frequently_atTop_fermatPsp {b : ℕ} (h : 1 ≤ b) : ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b

theorem Nat.infinite_setOf_pseudoprimes {b : ℕ} (h : 1 ≤ b) : {n : ℕ | n.FermatPsp b}.Infinite

Infinite set variant of Nat.exists_infinite_pseudoprimes