### Install Git Pre-push Hook

Source: https://github.com/imperialcollegelondon/flt/blob/main/CONTRIBUTING.md

Installs a Git pre-push hook to automatically run checks before each push, reducing CI failures. Execute this script in your local repository.

```bash
scripts/install_pre-push.sh
```

--------------------------------

### FLT Project Build and Check Commands

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Provides shell commands for building the FLT project and running pre-push checks.

```bash
# Build the project
lake build

# Run pre-push checks
scripts/run_before_push.sh

# Install pre-push hook
scripts/install_pre-push.sh
```

--------------------------------

### FLT Project Configuration (lakefile.toml)

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Configures the FLT project using the Lake build system. Specifies project name, default targets, Lean options, and dependencies on mathlib and checkdecls.

```toml
# lakefile.toml
name = "FLT"
defaultTargets = ["FLT"]
lintDriver = "batteries/runLinter"

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false
maxSynthPendingDepth = 3
weak.linter.mathlibStandardSet = true
warn.sorry = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

[[lean_lib]]
name = "FLT"
globs = ["FLT", "FermatsLastTheorem"]
```

--------------------------------

### Prove Non-existence of Frey Package in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Proves that no Frey package can exist, which is a key step in the proof of Fermat's Last Theorem. This theorem uses `Wiles_Frey` and `Mazur_Frey`.

```lean
-- Example: constructing a Frey package from a counterexample
lemma FreyPackage.of_not_FermatLastTheorem
    (h : ¬ FermatLastTheorem) : Nonempty FreyPackage

-- The key theorem: no Frey package exists
theorem FreyPackage.false (P : FreyPackage) : False := by
  apply Wiles_Frey P    -- p-torsion is not irreducible
  exact Mazur_Frey P    -- but Mazur says it is irreducible
```

--------------------------------

### Define Frey Package Structure in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines the `FreyPackage` structure, bundling counterexample data for FLT with conditions for Frey curve construction. This definition is crucial for applying Mazur's theorem.

```lean
import FLT.Basic.FreyPackage

/--
A *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying a^p + b^p = c^p and additional conditions
guaranteeing Section 4.1 of Serre's paper applies
to the curve Y^2 = X(X-a^p)(X+b^p).
-/ 
structure FreyPackage where
  a : ℤ
  b : ℤ
  c : ℤ
  ha0 : a ≠ 0
  hb0 : b ≠ 0
  hc0 : c ≠ 0
  p : ℕ
  pp : Nat.Prime p
  hp5 : 5 ≤ p
  hFLT : a ^ p + b ^ p = c ^ p
  hgcdab : gcd a b = 1
  ha4 : (a : ZMod 4) = 3
  hb2 : (b : ZMod 2) = 0
```

--------------------------------

### Run Pre-push Checks Manually

Source: https://github.com/imperialcollegelondon/flt/blob/main/CONTRIBUTING.md

Manually executes pre-push checks to reduce the risk of CI failures. This script requires manual execution before pushing changes.

```bash
scripts/run_before_push.sh
```

--------------------------------

### Model Elliptic Curve Torsion and Galois Action

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Provides definitions for n-torsion subgroups of elliptic curves and the resulting Galois representations.

```lean
import FLT.EllipticCurve.Torsion

variable {k : Type*} [Field k] (E : WeierstrassCurve k) [E.IsElliptic]

-- n-torsion subgroup of elliptic curve points
abbrev WeierstrassCurve.n_torsion (n : ℕ) : Type :=
  Submodule.torsionBy ℤ (E ⟮k⟯) n

-- n-torsion has ZMod n module structure
noncomputable instance (n : ℕ) : Module (ZMod n) (E.n_torsion n)

-- Over separably closed fields, |E[n]| = n²
theorem WeierstrassCurve.n_torsion_card [IsSepClosed k] {n : ℕ}
    (hn : (n : k) ≠ 0) : Nat.card (E.n_torsion n) = n^2

-- n-torsion is isomorphic to (ZMod n)²
theorem WeierstrassCurve.n_torsion_dimension [IsSepClosed k] {n : ℕ}
    (hn : (n : k) ≠ 0) :
    Nonempty (E.n_torsion n ≃+ (ZMod n) × (ZMod n))

-- Galois action on elliptic curve points
noncomputable def WeierstrassCurve.galoisRepresentation
    (K : Type*) [Field K] [Algebra k K] :
    DistribMulAction (K ≃ₐ[k] K) (E ⟮K⟯)

-- The continuous Galois representation from p-torsion
def WeierstrassCurve.galoisRep (E : WeierstrassCurve K) [E.IsElliptic]
    (n : ℕ) (hn : 0 < n) :
    GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)
```

--------------------------------

### Declare Fermat's Last Theorem in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Declares Fermat's Last Theorem for positive naturals. The proof relies on the `Wiles_Taylor_Wiles` definition. Check axioms used for proof.

```lean
import FLT

/-- Fermat's Last Theorem for positive naturals. -/
theorem PNat.pow_add_pow_ne_pow
    (x y z : ℕ+)
    (n : ℕ) (hn : n > 2) :
    x^n + y^n ≠ z^n :=
  PNat.pow_add_pow_ne_pow_of_FermatLastTheorem Wiles_Taylor_Wiles x y z n hn

-- Check axioms used in the proof
#print axioms PNat.pow_add_pow_ne_pow
-- Output: depends on [propext, sorryAx, Classical.choice, Quot.sound]
-- Project complete when `sorryAx` is removed
```

--------------------------------

### Use 'knownin1980s' Axiom in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Provides an axiom to assert propositions known before 1990, serving as a placeholder for full proofs. Requires comments explaining the mathematical justification. Can be used as a tactic.

```lean
import FLT.Assumptions.KnownIn1980s

/-- `knownin1980s` proves arbitrary propositions representing
    results deducible from pre-1990 literature. Must include
    comments explaining the mathematical justification. -/
axiom knownin1980s {P : Prop} : P

-- Usage as a tactic
macro "knownin1980s" : tactic => `(tactic| exact knownin1980s)

-- Example usage with required justification:
theorem Mazur_Frey (P : FreyPackage) :
    GaloisRep.IsIrreducible (P.freyCurve.galoisRep P.p P.hppos) := by
  -- This follows from Mazur's theorem on rational isogenies
  -- Reference: Mazur, "Modular curves and the Eisenstein ideal" (1978)
  knownin1980s
```

--------------------------------

### Define Galois Representations in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines the GaloisRep structure and associated operations like mapping, conjugation, and base change for Galois representations.

```lean
import FLT.Deformations.RepresentationTheory.GaloisRep

/-- `GaloisRep K A M` are A-linear galois reps of field K on A-module M. -/
def GaloisRep (K A M : Type*) [Field K] [NumberField K]
    [CommRing A] [TopologicalSpace A] [AddCommGroup M] [Module A M] :=
  Γ K →ₜ* Module.End A M

-- Field extension induces a map between galois reps
noncomputable def GaloisRep.map (ρ : GaloisRep K A M) (f : K →+* L) :
    GaloisRep L A M :=
  ρ.comp (Field.absoluteGaloisGroup.map f)

-- Conjugation by linear isomorphism
noncomputable def GaloisRep.conj (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) :
    GaloisRep K A N :=
  e'.toContinuousAlgHom.toContinuousMonoidHom.comp ρ

-- Framed galois rep with distinguished basis
abbrev FramedGaloisRep (K A n : Type*) := GaloisRep K A (n → A)

-- Equivalence with continuous homs into GL_n(A)
noncomputable def FramedGaloisRep.GL :
    FramedGaloisRep K A n ≃ (Γ K →ₜ* GL n A)

-- Base change for galois representations
noncomputable def GaloisRep.baseChange (B : Type*) [Algebra A B]
    (ρ : GaloisRep K A M) : GaloisRep K B (B ⊗[A] M)

-- Irreducibility of a Galois representation
def GaloisRep.IsIrreducible {k : Type*} [Field k]
    (ρ : GaloisRep K k M) : Prop :=
  ρ.toRepresentation.IsIrreducible
```

--------------------------------

### Define Frey Curve (Rational Coefficients) in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines the `freyCurve` for a `FreyPackage` over rationals. This is the elliptic curve associated with the Frey package.

```lean
/- The elliptic curve over ℚ associated to a Frey package. -/
def freyCurve (P : FreyPackage) : WeierstrassCurve ℚ where
  a₁ := 1
  a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4
  a₃ := 0
  a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16
  a₆ := 0
```

--------------------------------

### Define Weight 2 Automorphic Forms

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines the structure of weight-two automorphic forms on totally definite quaternion algebras, including adelic group actions.

```lean
import FLT.AutomorphicForm.QuaternionAlgebra.Defs

variable (F : Type*) [Field F] [NumberField F]
variable (D : Type*) [Ring D] [Algebra F D] [FiniteDimensional F D]

namespace TotallyDefiniteQuaternionAlgebra

-- (D ⊗ A_F^∞)ˣ - the adelic group
abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ

-- Inclusion of Dˣ into adelic group
noncomputable abbrev incl₁ : Dˣ →* Dfx F D

-- Inclusion of A_F^∞ˣ into adelic group
noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 F) F)ˣ →* Dfx F D

/-- Weight 2 automorphic form on totally definite quaternion algebra.
    Functions φ : Dˣ \ (D ⊗ A_F^∞)ˣ → R with level structure. -/
structure WeightTwoAutomorphicForm (R : Type*) [AddCommMonoid R] where
  toFun : Dfx F D → R
  left_invt : ∀ (δ : Dˣ) (g : Dfx F D), toFun (incl₁ F D δ * g) = toFun g
  right_invt : ∃ (U : Subgroup (Dfx F D)), IsOpen (U : Set (Dfx F D)) ∧
    ∀ g u, u ∈ U → toFun (g * u) = toFun g
  trivial_central_char : ∀ z g, toFun (g * incl₂ F D z) = toFun g

-- Automorphic forms have module structure
instance : Module R (WeightTwoAutomorphicForm F D R)

-- Adelic group action on automorphic forms
instance : DistribMulAction (Dfx F D) (WeightTwoAutomorphicForm F D R)

/-- Automorphic forms of fixed level U -/
def WeightTwoAutomorphicFormOfLevel (U : Subgroup (Dfx F D)) (R : Type*) :=
  MulAction.FixedPoints U (WeightTwoAutomorphicForm F D R)

end TotallyDefiniteQuaternionAlgebra
```

--------------------------------

### Compute Frey Curve j-invariant in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Provides the formula for the j-invariant of the Frey curve associated with a `FreyPackage`. The formula depends on `a`, `b`, `c`, and `p`.

```lean
-- The j-invariant formula
lemma FreyCurve.j (P : FreyPackage) :
    P.freyCurve.j = 2^8*(P.c^(2*P.p)-(P.a*P.b)^P.p)^3 / (P.a*P.b*P.c)^(2*P.p)
```

--------------------------------

### Define Frey Curve (Integer Coefficients) in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines the `freyCurveInt` for a `FreyPackage` over integers. It uses a change of variables for semistability at 2.

```lean
import FLT.Basic.FreyPackage

namespace FreyPackage

/-- The Weierstrass curve over ℤ associated to a Frey package.
    Uses change of variables X=4x, Y=8y+4x for semistability at 2. -/ 
def freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ where
  a₁ := 1
  a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4
  a₃ := 0
  a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16
  a₆ := 0
```

--------------------------------

### Define Automorphic Galois Representation in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Defines a 2-dimensional Galois representation as automorphic of level S. Requires a weight 2 automorphic form on a totally definite quaternion algebra. Used for modularity lifting theorems.

```lean
import FLT.GaloisRepresentation.Automorphic

/-- A 2-dimensional Galois rep is automorphic of level S if it comes from
    a weight 2 automorphic form on a totally definite quaternion algebra. -/
def GaloisRep.IsAutomorphicOfLevel
    {F : Type*} [Field F] [NumberField F] [IsTotallyReal F]
    (p : ℕ) [Fact p.Prime]
    {A : Type*} [CommRing A] [Algebra ℤ_[p] A]
    {V : Type*} [AddCommGroup V] [Module A V] [Module.Free A V]
    (hV : Module.finrank A V = 2)
    (ρ : GaloisRep F A V)
    (S : Finset (HeightOneSpectrum (𝓞 F))) : Prop :=
  ∃ (D : Type*) (_ : Ring D) (_ : Algebra F D) (_ : IsQuaternionAlgebra F D)
    (r : IsQuaternionAlgebra.NumberField.Rigidification F D)
    (π : HeckeAlgebra F D r S ℤ_[p] →ₐ[ℤ_[p]] A),
  ∀ v : HeightOneSpectrum (𝓞 F), ↑p ∉ v.1 → v ∉ S →
    ρ.IsUnramifiedAt v ∧
    (ρ.toLocal v (Frob v)).det = v.1.absNorm ∧
    LinearMap.trace A V (ρ.toLocal v (Frob v)) = π (HeckeAlgebra.T D r ℤ_[p] v _)
```

```lean
-- Cyclic base change theorem (key for modularity lifting)
theorem cyclic_base_change
    {F : Type*} [Field F] [NumberField F] [IsTotallyReal F]
    (hF : Even (Module.finrank ℚ F))
    {E : Type*} [Field E] [NumberField E] [IsTotallyReal E]
    [Algebra F E] [IsGalois F E] [IsSolvable (E ≃ₐ[F] E)]
    (p : ℕ) [Fact p.Prime]
    (ρ : GaloisRep F (ℚ_[p]ᵃˡᵍ) V)
    (hρirred : GaloisRep.IsIrreducible (ρ.map (algebraMap F E))) -- ... additional hypotheses ...
    (S : Finset (HeightOneSpectrum (𝓞 F))) :
    (ρ.IsAutomorphicOfLevel p hV S) ↔
    ((ρ.map (algebraMap F E)).IsAutomorphicOfLevel p hV
      (HeightOneSpectrum.preimageComapFinset (𝓞 F) F E (𝓞 E) S))
```

--------------------------------

### Compute Frey Curve Discriminant in Lean

Source: https://context7.com/imperialcollegelondon/flt/llms.txt

Computes the discriminant `Δ` for the Frey curve associated with a `FreyPackage`. The formula involves the terms `a`, `b`, `c`, and `p` from the package.

```lean
-- The discriminant computation
lemma FreyCurve.Δ (P : FreyPackage) :
    P.freyCurve.Δ = (P.a*P.b*P.c)^(2*P.p) / 2 ^ 8
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.