Fermat Pseudoprimes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

fermat_psp.probable_prime: 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
fermat_psp: 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 definiton of probable_prime 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

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

source

def fermat_psp.probable_prime (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

fermat_psp.probable_prime n b = (n ∣ b ^ (n - 1) - 1)

Instances for fermat_psp.probable_prime

fermat_psp.decidable_probable_prime

source

def fermat_psp (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

fermat_psp n b = (fermat_psp.probable_prime n b ∧ ¬nat.prime n ∧ 1 < n)

Instances for fermat_psp

fermat_psp.decidable_psp

source

@[protected, instance]

def fermat_psp.decidable_probable_prime (n b : ℕ) :

decidable (fermat_psp.probable_prime n b)

Equations

fermat_psp.decidable_probable_prime n b = nat.decidable_dvd n (b ^ (n - 1) - 1)

source

@[protected, instance]

def fermat_psp.decidable_psp (n b : ℕ) :

decidable (fermat_psp n b)

Equations

fermat_psp.decidable_psp n b = and.decidable

source

theorem fermat_psp.coprime_of_probable_prime {n b : ℕ} (h : fermat_psp.probable_prime n 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.

source

theorem fermat_psp.probable_prime_iff_modeq (n : ℕ) {b : ℕ} (h : 1 ≤ b) :

fermat_psp.probable_prime n b ↔ b ^ (n - 1) ≡ 1 [MOD n]

source

theorem fermat_psp.coprime_of_fermat_psp {n b : ℕ} (h : fermat_psp n 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_probable_prime

source

theorem fermat_psp.base_one {n : ℕ} (h₁ : 1 < n) (h₂ : ¬nat.prime n) :

fermat_psp n 1

All composite numbers are Fermat pseudoprimes to base 1.

source

theorem fermat_psp.exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) :

∃ (n : ℕ), fermat_psp n b ∧ m ≤ n

For all positive bases, there exist Fermat infinite 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.

source

theorem fermat_psp.frequently_at_top_fermat_psp {b : ℕ} (h : 1 ≤ b) :

∃ᶠ (n : ℕ) in filter.at_top , fermat_psp n b

source

theorem fermat_psp.infinite_set_of_prime_modeq_one {b : ℕ} (h : 1 ≤ b) :

{n : ℕ | fermat_psp n b}.infinite

Infinite set variant of exists_infinite_pseudoprimes