Trough

First reductions of the problem

Initializing search

Home
Mathematics

Trough

Home
Mathematics
Mathematics
- Trough
  Trough
  - Mathlib
  - Tau Ceti
  - Fermat's Last Theorem (Imperial)
    
    Fermat's Last Theorem (Imperial)
    
    Introduction
    
    First reductions of the problem
    
    First reductions of the problem
    
    Goal
    
    Overview
    
    Reduction to n ≥ 5 and prime
    
    Frey packages
    
    Galois representations and elliptic curves
    
    The Frey curve
    
    Reduction to two big theorems.
    
    Reducibility of p-torsion of the Frey curve
    
    An example of an automorphic form
    
    Automorphic forms and the Langlands Conjectures
    
    Miniproject: Frobenius elements
    
    Miniproject: Adeles
    
    Miniproject: Haar Characters
    
    Miniproject: Fujisaki's Lemma
    
    Miniproject: Quaternion algebras
    
    Miniproject: Hecke Operators
  - PNT+
  - Polynomial Freiman-Ruzsa
  - Equational Theories
  - Strong PNT (Math Inc)
  - Formal Conjectures
  - Fermat's Last Theorem (Anthropic)
  - Classification of Finite Simple Groups (Axiom)
  - Lean Pool
  - Formal Frontier
  - Coverage
  - Sources

Home
Trough
Fermat's Last Theorem (Imperial)
First reductions of the problem

Loading the map…

← First reductions of the problem

First reductions of the problem

Goal
Overview
Reduction to \(n\geq5\) and prime
Frey packages
Galois representations and elliptic curves
The Frey curve
Reduction to two big theorems.

Loading dependency explorer…

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Developed with AutoformBot. Formalization source. Articles written for Trough are available under CC BY-SA 4.0; Mathlib's docstrings and signatures under Apache-2.0.