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

• FermatLastTheoremWith R n: The statement that only solutions to the Fermat equation a^n + b^n = c^n in the semiring R have a = 0, b = 0 or c = 0.

  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.

• FermatLastTheoremFor n : The statement that the only solutions to a^n + b^n = c^n in ℕ have a = 0, b = 0 or c = 0. Again, this statement is not always true, for example FermatLastTheoremFor 1 is false because 2^1 + 2^1 = 4^1.

• FermatLastTheorem : The statement of Fermat's Last Theorem, namely that the only solutions to a^n + b^n = c^n in ℕ when n ≥ 3 have a = 0, b = 0 or c = 0.

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][Wiles-FLT] and [R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras][Taylor-Wiles-FLT]). An ongoing Lean formalisation of the proof, using mathlib as a dependency, is taking place at https://github.com/ImperialCollegeLondon/FLT .

def FermatLastTheoremWith (R : Type u_1) [Semiring R] (n : ℕ) : Prop

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

Equations

• FermatLastTheoremWith R n = ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

def FermatLastTheoremFor (n : ℕ) : Prop

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

Equations

• FermatLastTheoremFor n = FermatLastTheoremWith ℕ n

def FermatLastTheorem : Prop

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

• FermatLastTheorem = ∀ n ≥ 3, FermatLastTheoremFor n

theorem fermatLastTheoremFor_zero : FermatLastTheoremFor 0

theorem not_fermatLastTheoremFor_one : ¬FermatLastTheoremFor 1

theorem not_fermatLastTheoremFor_two : ¬FermatLastTheoremFor 2

theorem FermatLastTheoremWith.mono {R : Type u_1} [Semiring R] [NoZeroDivisors R] {m n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremWith R m) : FermatLastTheoremWith R n

theorem FermatLastTheoremFor.mono {m n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremFor m) : FermatLastTheoremFor n

theorem fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

theorem fermatLastTheoremFor_iff_nat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n

theorem fermatLastTheoremFor_iff_int {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n

theorem fermatLastTheoremFor_iff_rat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n

def FermatLastTheoremWith' (R : Type u_2) [CommSemiring R] (n : ℕ) : Prop

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' R is weaker than FermatLastTheoremWith R in general. In particular, it holds trivially for [Field R].
2. This variant is equivalent to the original FermatLastTheoremWith R for R = ℕ or ℤ. In general, they are equivalent if there is no solutions of units to the Fermat equation.
3. For a polynomial ring R = k[X], the original FermatLastTheoremWith R is false but the weaker variant FermatLastTheoremWith' R 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.

theorem FermatLastTheoremWith.fermatLastTheoremWith' {R : Type u_2} [CommSemiring R] {n : ℕ} (h : FermatLastTheoremWith R n) : FermatLastTheoremWith' R n

theorem fermatLastTheoremWith'_of_semifield (𝕜 : Type u_2) [Semifield 𝕜] (n : ℕ) : FermatLastTheoremWith' 𝕜 n

theorem FermatLastTheoremWith'.fermatLastTheoremWith {R : Type u_2} [CommSemiring R] [IsDomain R] {n : ℕ} (h : FermatLastTheoremWith' R n) (hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith R n

theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith {R : Type u_2} [CommSemiring R] [IsDomain R] {n : ℕ} (hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith' R n ↔ FermatLastTheoremWith R n

theorem fermatLastTheoremWith'_nat_int_tfae (n : ℕ) : [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE

theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : ℕ} {R : Type u_2} [CommSemiring R] [IsDomain R] [DecidableEq R] [NormalizedGCDMonoid R] (hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith R 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) : IsCoprime a b