Documentation

Mathlib.NumberTheory.FermatPsp

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

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

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

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)
Instances For
    def Nat.FermatPsp (n : ) (b : ) :

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