Fermat's Last Theorem in Lean 4

← all areas

Namespace LanglandsTunnell 1,543 theorems

Landmarks here: Weight-one form attached to a surjective mod-3 representation

215 · ArchBessel 11 · ArchPlace 7 · Artin 11 · Converse 173 · CubicInduction 656 · CubicLambda 9 · ExplicitLift 4 · HeckeTate 5 · P2 21 · RankinSelberg 339 · RealArchParam 1 · TateLocal 91

directly in LanglandsTunnell 215

LanglandsTunnell.ArchBessel 11

LanglandsTunnell.ArchPlace 7

LanglandsTunnell.Artin 11

LanglandsTunnell.Converse 173

LanglandsTunnell.CubicInduction 656

LanglandsTunnell.CubicLambda 9

LanglandsTunnell.ExplicitLift 4

LanglandsTunnell.HeckeTate 5

LanglandsTunnell.P2 21

LanglandsTunnell.RankinSelberg 339

LanglandsTunnell.RealArchParam 1

LanglandsTunnell.TateLocal 91