Reductions

📁 Source: FLT/Basic/Reductions.lean

Statistics

Metric	Count
Definitions instDecidableEqAlgebraicClosureRat_fLT_1	1
Theorems false, Mazur_Frey, Wiles_Frey, Wiles_Taylor_Wiles	4
Total	5
⚠️ With sorry Mazur_Frey	1

FreyPackage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
false 📖	—	—	—	—	Wiles_Frey Mazur_Frey

(root)

Definitions

Name	Category	Theorems
instDecidableEqAlgebraicClosureRat_fLT_1 📖	CompOp	2 math math: Mazur_Frey, Wiles_Frey

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Mazur_Frey 📖 ⚠️	mathematical	—	GaloisRep.IsIrreducible WeierstrassCurve.n_torsion FreyPackage.freyCurve instDecidableEqAlgebraicClosureRat_fLT_1 FreyPackage.p FreyPackage.pp instModuleZModN_torsion WeierstrassCurve.galoisRep FreyCurve.instIsEllipticRatFreyCurve FreyPackage.hppos	—	FreyPackage.pp FreyCurve.instIsEllipticRatFreyCurve FreyPackage.hppos
Wiles_Frey 📖	mathematical	—	GaloisRep.IsIrreducible WeierstrassCurve.n_torsion FreyPackage.freyCurve instDecidableEqAlgebraicClosureRat_fLT_1 FreyPackage.p FreyPackage.pp instModuleZModN_torsion WeierstrassCurve.galoisRep FreyCurve.instIsEllipticRatFreyCurve FreyPackage.hppos	—	FreyCurve.torsion_not_isIrreducible
Wiles_Taylor_Wiles 📖	—	—	—	—	FreyPackage.of_not_FermatLastTheorem FreyPackage.false

---

← Back to Index