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 #

source
def Nat.fermatNumber (n : ℕ) :
ℕ

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

Equations
  • n.fermatNumber = 2 ^ 2 ^ n + 1
Instances For
    source
    @[simp]
    theorem Nat.fermatNumber_zero :
    Nat.fermatNumber 0 = 3
    source
    @[simp]
    theorem Nat.fermatNumber_one :
    Nat.fermatNumber 1 = 5
    source
    @[simp]
    theorem Nat.fermatNumber_two :
    Nat.fermatNumber 2 = 17
    source
    theorem Nat.strictMono_fermatNumber :
    StrictMono Nat.fermatNumber
    source
    theorem Nat.two_lt_fermatNumber (n : ℕ) :
    2 < n.fermatNumber
    source
    theorem Nat.odd_fermatNumber (n : ℕ) :
    Odd n.fermatNumber
    source
    theorem Nat.fermatNumber_product (n : ℕ) :
    ∏ k ∈ Finset.range n, k.fermatNumber = n.fermatNumber - 2
    source
    theorem Nat.fermatNumber_eq_prod_add_two (n : ℕ) :
    n.fermatNumber = ∏ k ∈ Finset.range n, k.fermatNumber + 2
    source
    theorem Nat.fermatNumber_succ (n : ℕ) :
    (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1
    source
    theorem Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ℕ) :
    2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2
    source
    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
    source
    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
    source
    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].