From 2f7a000681c535f100b666650cbb2e0fb9c3a78d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 20 Mar 2024 18:25:54 +0000 Subject: [PATCH] more tidying of Reductions.lean --- FLT/Basic/Reductions.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean index 8f15de65..140f0971 100644 --- a/FLT/Basic/Reductions.lean +++ b/FLT/Basic/Reductions.lean @@ -8,8 +8,11 @@ import Mathlib.RingTheory.SimpleModule /-! -This file proves many of the key results which reduce Fermat's Last Theorem -to Mazur's theorem and the Wiles-Taylor-Wiles theorem. + +# Preliminary reductions of FLT + +This file proves some of the key results which reduce Fermat's Last Theorem +to Mazur's theorem and the Wiles/Taylor--Wiles theorem. # Main definitions @@ -18,7 +21,7 @@ $(a,b,c)$ and a prime $p \geq 5$ such that $a^p+b^p=c^p$ and furthermore such that $a$ is 3 mod 4 and $b$ is 0 mod 2. The motivation behind this definition is that then all the results in Section 4.1 -of Serre's paper [Serre] apply to the elliptic curve curve $Y^2=X(X-a^p)(X+b^p).$ +of Serre's paper [Serre] apply to the elliptic curve $Y^2=X(X-a^p)(X+b^p).$ # Main theorems @@ -54,11 +57,12 @@ lemma fermatLastTheoremThree : FermatLastTheoremFor 3 := sorry namespace FLT -/-! +/- We continue with the reduction of Fermat's Last Theorem. -/ + /-- If Fermat's Last Theorem is false, there's a nontrivial solution to a^p+b^p=c^p with p>=5 prime. -/ lemma p_ge_5_counterexample_of_not_FermatLastTheorem (h : ¬ FermatLastTheorem) : ∃ (a b c : ℤ) (_ : a ≠ 0) (_ : b ≠ 0) (_ : c ≠ 0) (p : ℕ) (_ : p.Prime) (_ : 5 ≤ p),