mathlib3 documentation

number_theory.fermat_psp

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

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

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
Instances for fermat_psp.probable_prime
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
Instances for fermat_psp
@[protected, instance]
Equations
theorem fermat_psp.coprime_of_probable_prime {n b : } (h : fermat_psp.probable_prime n b) (h₁ : 1 n) (h₂ : 1 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 fermat_psp.probable_prime_iff_modeq (n : ) {b : } (h : 1 b) :
theorem fermat_psp.coprime_of_fermat_psp {n b : } (h : fermat_psp n b) (h₁ : 1 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

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

All composite numbers are Fermat pseudoprimes to base 1.

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.

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