Documentation

Mathlib.NumberTheory.FLT.Basic

Statement of Fermat's Last Theorem #

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

Main definitions #

Note that this statement can certainly be false for certain values of R and n. For example FermatLastTheoremWith ℝ 3 is false as 1^3 + 1^3 = (2^{1/3})^3, and FermatLastTheoremWith ℕ 2 is false, as 3^2 + 4^2 = 5^2.

History #

Fermat's Last Theorem was an open problem in number theory for hundreds of years, until it was finally solved by Andrew Wiles, assisted by Richard Taylor, in 1994 (see A. Wiles, Modular elliptic curves and Fermat's last theorem and R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras). An ongoing Lean formalisation of the proof, using mathlib as a dependency, is taking place at https://github.com/ImperialCollegeLondon/FLT .

def FermatLastTheoremWith (α : Type u_1) [Semiring α] (n : ) :

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Equations
Instances For

    Statement of Fermat's Last Theorem over the naturals for a given exponent.

    Equations
    Instances For

      Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial natural solution when n ≥ 3.

      This is now a theorem of Wiles and Taylor--Wiles; see https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of a proof.

      Equations
      Instances For
        theorem FermatLastTheoremWith.mono {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m : } {n : } (hmn : m n) (hm : FermatLastTheoremWith α m) :
        def FermatLastTheoremWith' (α : Type u_2) [CommSemiring α] (n : ) :

        A relaxed variant of Fermat's Last Theorem over a given commutative semiring with a specific exponent, allowing nonzero solutions of units and their common multiples.

        1. The variant FermatLastTheoremWith' α is weaker than FermatLastTheoremWith α in general. In particular, it holds trivially for [Field α].
        2. This variant is equivalent to the original FermatLastTheoremWith α for α = ℕ or . In general, they are equivalent if there is no solutions of units to the Fermat equation.
        3. For a polynomial ring α = k[X], the original FermatLastTheoremWith α is false but the weaker variant FermatLastTheoremWith' α is true. This polynomial variant of Fermat's Last Theorem can be shown elementarily using Mason--Stothers theorem.
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem FermatLastTheoremWith'.fermatLastTheoremWith {α : Type u_2} [CommSemiring α] [IsDomain α] {n : } (h : FermatLastTheoremWith' α n) (hn : ∀ (a b c : α), IsUnit aIsUnit bIsUnit ca ^ n + b ^ n c ^ n) :
          theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith {α : Type u_2} [CommSemiring α] [IsDomain α] {n : } (hn : ∀ (a b c : α), IsUnit aIsUnit bIsUnit ca ^ n + b ^ n c ^ n) :
          theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : } {R : Type u_2} [CommSemiring R] [IsDomain R] [DecidableEq R] [NormalizedGCDMonoid R] (hn : ∀ (a b c : R), a 0b 0c 0{a, b, c}.gcd id = 1a ^ n + b ^ n c ^ n) :

          To prove Fermat Last Theorem in any semiring that is a NormalizedGCDMonoid one can assume that the gcd of {a, b, c} is 1.

          theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : } {p : } (hp : Prime p) {a : } {b : } {c : } (hpa : p a) (hpb : p b) (HF : a ^ n + b ^ n + c ^ n = 0) :
          p c
          theorem isCoprime_of_gcd_eq_one_of_FLT {n : } {a : } {b : } {c : } (Hgcd : {a, b, c}.gcd id = 1) (HF : a ^ n + b ^ n + c ^ n = 0) :