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 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 : ℕ) : Prop

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

Equations

• FermatLastTheoremWith α n = ∀ (a b c : α), 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 {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) : FermatLastTheoremWith α 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' (α : Type u_2) [CommSemiring α] (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' α 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.

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

theorem fermatLastTheoremWith'_of_field (α : Type u_2) [Field α] (n : ℕ) : FermatLastTheoremWith' α n

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

theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith {α : Type u_2} [CommSemiring α] [IsDomain α] {n : ℕ} (hn : ∀ (a b c : α), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith' α n ↔ FermatLastTheoremWith α 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