2. Frey package

2. Frey package. A Frey package (Definitions/Def_FLTPrelim_FreyPackage.lean, adapted from the Imperial College London FLT project) is a solution a^p + b^p = c^p in nonzero integers, p ≥ 5 prime, normalised to gcd(a,b) = 1, a ≡ 3 (mod 4), 2 | b, with the Frey curve E_P : y² + xy = x³ + ((b^p − 1 − a^p)/4)x² − (a^p b^p/16)x, an integral model of y² = x(x − a^p)(x + b^p). FreyPackage.of_counterexample builds one from any counterexample in nonzero integers with prime exponent p ≥ 5 (citing only Mathlib); FreyPackage.no_frey_package (P : FreyPackage) : False is assembled from exactly the four theorems of steps 3 to 6: irreducible and modular gives, after level lowering, a nonzero weight-2 cusp form on Γ₀(2), and there is none.

Quoted from the route of the proof in PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

The landmarks the repository's web pages place in this step, in the order this step names them:

TheoremFreyPackage.of_counterexample#

theorem FreyPackage.of_counterexample (a b c : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (p : ℕ) (pp : p.Prime) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackage

Quoted from Theorems/Thm_FreyPackage_of_counterexample.lean, line 6 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Frey curve”, “Frey”.

PROOF-PATH.md names it in 1. Reduction to a prime p ≥ 5 and 2. Frey package.

Lean

FreyPackage.of_counterexample, stated in Theorems/Thm_FreyPackage_of_counterexample.lean, line 6 and proved in P2M/Sol/S_FreyPackage_of_counterexample.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.of_counterexample in Theorems/Thm_FreyPackage_of_counterexample.lean
• Proof of FreyPackage.of_counterexample in P2M/Sol/S_FreyPackage_of_counterexample.lean
• The repository's documentation page for FreyPackage.of_counterexample

LeanFreyPackage.of_counterexample

Used by 1

Used byFreyPackage.fermatLastTheoremFor_of_five_le

TheoremFreyPackage.no_frey_package#

theorem FreyPackage.no_frey_package (P : FreyPackage) : False

Quoted from Theorems/Thm_FreyPackage_no_frey_package.lean, line 129 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Frey”, “Serre”, “Ribet”, “Wiles”, “four-way contradiction”.

PROOF-PATH.md names it in 1. Reduction to a prime p ≥ 5 and 2. Frey package.

Lean

FreyPackage.no_frey_package, stated in Theorems/Thm_FreyPackage_no_frey_package.lean, line 129 and proved in P2M/Sol/S_FreyPackage_no_frey_package.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of FreyPackage.no_frey_package in Theorems/Thm_FreyPackage_no_frey_package.lean
• Proof of FreyPackage.no_frey_package in P2M/Sol/S_FreyPackage_no_frey_package.lean
• The repository's documentation page for FreyPackage.no_frey_package

LeanFreyPackage.no_frey_package

Uses 4 · Used by 1

Proof usesIrreducibility · Modularity · Level lowering · S₂(Γ₀(2)) = 0

Used byFreyPackage.fermatLastTheoremFor_of_five_le

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.