Documentation

Mathlib.NumberTheory.Fermat

Fermat numbers #

The Fermat numbers are a sequence of natural numbers defined as Nat.fermatNumber n = 2^(2^n) + 1, for all natural numbers n.

Main theorems #

Fermat numbers: the n-th Fermat number is defined as 2^(2^n) + 1.

Equations
  • n.fermatNumber = 2 ^ 2 ^ n + 1
Instances For
    theorem Nat.two_lt_fermatNumber (n : ) :
    2 < n.fermatNumber
    theorem Nat.odd_fermatNumber (n : ) :
    Odd n.fermatNumber
    theorem Nat.fermatNumber_product (n : ) :
    kFinset.range n, k.fermatNumber = n.fermatNumber - 2
    theorem Nat.fermatNumber_eq_prod_add_two (n : ) :
    n.fermatNumber = kFinset.range n, k.fermatNumber + 2
    theorem Nat.fermatNumber_succ (n : ) :
    (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1
    theorem Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ) :
    2 * (n.fermatNumber - 1) ^ 2 (n + 1).fermatNumber ^ 2
    theorem Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ) :
    (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2
    theorem Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ) :
    (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2
    theorem Nat.coprime_fermatNumber_fermatNumber {k : } {n : } (h : k n) :
    n.fermatNumber.Coprime k.fermatNumber

    Goldbach's theorem : no two distinct Fermat numbers share a common factor greater than one.

    From a letter to Euler, see page 37 in [JW22].