Fermat's Last Theorem in Lean 4

Areas: the 331 top-level namespaces

Every theorem, grouped by the first component of its name. The namespace is the nearest thing the tree has to a table of contents by subject: ModularCurve and AlgebraicGeometry carry Mazur's argument and the modular-curve infrastructure, CerednikDrinfeld the uniformisation behind level lowering, LanglandsTunnell and AutomorphicForm the automorphic input to modularity, and so on. The "mostly under" column says which step of the route the members sit under (first landmark above them), as a rough guide.

namespacetheoremslandmarksmostly under
ModularCurve7,7112Modularity (Wiles, Taylor–Wiles) (3,995), Level lowering (Ribet) (1,975)
AlgebraicGeometry3,3220Level lowering (Ribet) (2,483), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (432)
CerednikDrinfeld2,3760Level lowering (Ribet) (2,376)
AutomorphicForm2,3361Modularity (Wiles, Taylor–Wiles) (2,336)
AlgebraicCurve1,5770Modularity (Wiles, Taylor–Wiles) (771), Level lowering (Ribet) (420)
LanglandsTunnell1,5431Modularity (Wiles, Taylor–Wiles) (1,543)
WeierstrassCurve1,00316Modularity (Wiles, Taylor–Wiles) (512), Level lowering (Ribet) (290)
NumberField7660Modularity (Wiles, Taylor–Wiles) (754), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (11)
CuspForm6921Modularity (Wiles, Taylor–Wiles) (609), Level lowering (Ribet) (65)
GoodReductionJacobian6740Level lowering (Ribet) (558), Modularity (Wiles, Taylor–Wiles) (72)
groupCohomology3610Modularity (Wiles, Taylor–Wiles) (361)
ValuationSubring3370Modularity (Wiles, Taylor–Wiles) (186), Level lowering (Ribet) (108)
HopfAlgebra3330Modularity (Wiles, Taylor–Wiles) (264), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (55)
Algebra3021Modularity (Wiles, Taylor–Wiles) (162), Level lowering (Ribet) (124)
QuaternionAlgebra3020Level lowering (Ribet) (302)
Module2120Level lowering (Ribet) (104), Modularity (Wiles, Taylor–Wiles) (72)
CohCarrier1920Modularity (Wiles, Taylor–Wiles) (188), Level lowering (Ribet) (4)
Rep1880Modularity (Wiles, Taylor–Wiles) (188)
IsLocalRing1810Modularity (Wiles, Taylor–Wiles) (123), Level lowering (Ribet) (49)
WeierstrassProjModel1730Modularity (Wiles, Taylor–Wiles) (165), Level lowering (Ribet) (8)
MvFormalGroup1660Level lowering (Ribet) (124), Modularity (Wiles, Taylor–Wiles) (42)
ModularForm1562Modularity (Wiles, Taylor–Wiles) (79), Level lowering (Ribet) (41)
M4aHerbrand1480Modularity (Wiles, Taylor–Wiles) (148)
PDivisibleGroup1380Modularity (Wiles, Taylor–Wiles) (138)
GaloisRepAdic1350Modularity (Wiles, Taylor–Wiles) (135)
MeasureTheory1320Modularity (Wiles, Taylor–Wiles) (129), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (3)
HeckeEis1300Modularity (Wiles, Taylor–Wiles) (117), Level lowering (Ribet) (12)
GaloisRep1271Modularity (Wiles, Taylor–Wiles) (104), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (19)
Deformation1200Modularity (Wiles, Taylor–Wiles) (120)
Matrix1050Modularity (Wiles, Taylor–Wiles) (60), Level lowering (Ribet) (42)
MvPolynomial990Level lowering (Ribet) (41), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (34)
(no namespace)984Modularity (Wiles, Taylor–Wiles) (47), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (34)
NeronModelInfra960Level lowering (Ribet) (88), Modularity (Wiles, Taylor–Wiles) (4)
Ideal940Modularity (Wiles, Taylor–Wiles) (53), Level lowering (Ribet) (31)
ResidualGaloisRep921Modularity (Wiles, Taylor–Wiles) (91), Level lowering (Ribet) (1)
ExtCitation850Modularity (Wiles, Taylor–Wiles) (72), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (13)
MvPowerSeries810Modularity (Wiles, Taylor–Wiles) (47), Level lowering (Ribet) (33)
FormalGroup780Modularity (Wiles, Taylor–Wiles) (78)
IsDiscreteValuationRing780Modularity (Wiles, Taylor–Wiles) (62), Level lowering (Ribet) (16)
Polynomial760Modularity (Wiles, Taylor–Wiles) (31), Level lowering (Ribet) (27)
DrinfeldCurve710Modularity (Wiles, Taylor–Wiles) (71)
ModPForms650Modularity (Wiles, Taylor–Wiles) (65)
Complex640Modularity (Wiles, Taylor–Wiles) (38), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (21)
Submodule620Level lowering (Ribet) (31), Modularity (Wiles, Taylor–Wiles) (17)
IntermediateField600Modularity (Wiles, Taylor–Wiles) (51), Level lowering (Ribet) (5)
FreyPackage5917Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (27), Level lowering (Ribet) (26)
LinearMap590Modularity (Wiles, Taylor–Wiles) (32), Level lowering (Ribet) (22)
IsDedekindDomain570Modularity (Wiles, Taylor–Wiles) (47), Level lowering (Ribet) (5)
TateCurve570Level lowering (Ribet) (22), Modularity (Wiles, Taylor–Wiles) (19)
LT500Modularity (Wiles, Taylor–Wiles) (44), Level lowering (Ribet) (6)
Representation500Modularity (Wiles, Taylor–Wiles) (44), Level lowering (Ribet) (4)
CuspidalType450Modularity (Wiles, Taylor–Wiles) (45)
PowerSeries440Level lowering (Ribet) (19), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (16)
RingHom410Modularity (Wiles, Taylor–Wiles) (27), Level lowering (Ribet) (8)
RubinSilverberg410Modularity (Wiles, Taylor–Wiles) (41)
IsRegularLocalRing390Modularity (Wiles, Taylor–Wiles) (25), Level lowering (Ribet) (12)
PadicAlgCl390Modularity (Wiles, Taylor–Wiles) (39)
AdicCompletion370Modularity (Wiles, Taylor–Wiles) (26), Level lowering (Ribet) (9)
TwoChartCech370Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (16), Level lowering (Ribet) (14)
ArtinL360Modularity (Wiles, Taylor–Wiles) (36)
Ihara360Modularity (Wiles, Taylor–Wiles) (34), Level lowering (Ribet) (2)
IsIntegrallyClosed320Level lowering (Ribet) (17), Modularity (Wiles, Taylor–Wiles) (15)
WittVector320Level lowering (Ribet) (23), Modularity (Wiles, Taylor–Wiles) (9)
AlgHom310Modularity (Wiles, Taylor–Wiles) (20), Level lowering (Ribet) (6)
Subalgebra290Modularity (Wiles, Taylor–Wiles) (13), Level lowering (Ribet) (12)
HeckeCharacter280Modularity (Wiles, Taylor–Wiles) (28)
UpperHalfPlane280Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (10), Modularity (Wiles, Taylor–Wiles) (9)
CongruenceSubgroup270Modularity (Wiles, Taylor–Wiles) (22), Level lowering (Ribet) (5)
PadicInt260Modularity (Wiles, Taylor–Wiles) (19), Level lowering (Ribet) (6)
CartierDual250Modularity (Wiles, Taylor–Wiles) (19), Level lowering (Ribet) (4)
EisensteinGeneral250Modularity (Wiles, Taylor–Wiles) (25)
DeligneSerre240Modularity (Wiles, Taylor–Wiles) (23), Level lowering (Ribet) (1)
IharaLemma240Modularity (Wiles, Taylor–Wiles) (24)
ProjSpaceCech240Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (15), Level lowering (Ribet) (9)
FrobeniusDensity230Modularity (Wiles, Taylor–Wiles) (21), Level lowering (Ribet) (2)
HopfOrder230Modularity (Wiles, Taylor–Wiles) (22), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
AddCommGroup220Level lowering (Ribet) (12), Modularity (Wiles, Taylor–Wiles) (6)
FrobeniusEndo220Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (15), Modularity (Wiles, Taylor–Wiles) (6)
LaurentSeries220Modularity (Wiles, Taylor–Wiles) (12), Level lowering (Ribet) (8)
LocalNewvector220Modularity (Wiles, Taylor–Wiles) (22)
HenselianLocalRing210Modularity (Wiles, Taylor–Wiles) (19), Level lowering (Ribet) (2)
LocalGL2210Modularity (Wiles, Taylor–Wiles) (20), Level lowering (Ribet) (1)
TwistedUnipotentTerm210Modularity (Wiles, Taylor–Wiles) (21)
FLT200Modularity (Wiles, Taylor–Wiles) (10), Level lowering (Ribet) (7)
FullLevelTate200Modularity (Wiles, Taylor–Wiles) (20)
HaarQuotient200Modularity (Wiles, Taylor–Wiles) (20)
Subgroup200Modularity (Wiles, Taylor–Wiles) (11), Level lowering (Ribet) (8)
TateModule200Modularity (Wiles, Taylor–Wiles) (16), Level lowering (Ribet) (4)
AddMonoidHom190Modularity (Wiles, Taylor–Wiles) (12), Level lowering (Ribet) (6)
Bialgebra190Modularity (Wiles, Taylor–Wiles) (17), Level lowering (Ribet) (1)
PeriodPair180Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (10), Modularity (Wiles, Taylor–Wiles) (6)
WLight180Level lowering (Ribet) (17), Modularity (Wiles, Taylor–Wiles) (1)
AddSubgroup170Modularity (Wiles, Taylor–Wiles) (9), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (7)
IharaTower170Modularity (Wiles, Taylor–Wiles) (17)
CategoryTheory150Level lowering (Ribet) (10), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (5)
DoubleComplex150Level lowering (Ribet) (15)
IsAdicComplete150Modularity (Wiles, Taylor–Wiles) (14), Level lowering (Ribet) (1)
ModularFormClass140Modularity (Wiles, Taylor–Wiles) (11), Level lowering (Ribet) (3)
UnramifiedWhittaker140Modularity (Wiles, Taylor–Wiles) (14)
ZMod140Modularity (Wiles, Taylor–Wiles) (7), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4)
HeckeCohomology130Modularity (Wiles, Taylor–Wiles) (13)
RegularSingular130Modularity (Wiles, Taylor–Wiles) (13)
W54130Modularity (Wiles, Taylor–Wiles) (13)
EisensteinSeries120Modularity (Wiles, Taylor–Wiles) (7), Level lowering (Ribet) (4)
IsCyclotomicExtension121Modularity (Wiles, Taylor–Wiles) (9), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (3)
MonoidHom120Modularity (Wiles, Taylor–Wiles) (10), Level lowering (Ribet) (2)
Padic120Modularity (Wiles, Taylor–Wiles) (7), Level lowering (Ribet) (5)
PadicComplex120Modularity (Wiles, Taylor–Wiles) (12)
V3Asm120Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (12)
AlgebraicClosure110Modularity (Wiles, Taylor–Wiles) (9), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
IsArtinianRing110Level lowering (Ribet) (7), Modularity (Wiles, Taylor–Wiles) (4)
IsPrimitiveRoot110Modularity (Wiles, Taylor–Wiles) (11)
V3AsmLevel110Level lowering (Ribet) (11)
AdjoinRoot100Modularity (Wiles, Taylor–Wiles) (6), Level lowering (Ribet) (4)
ContinuousLinearMap100Modularity (Wiles, Taylor–Wiles) (10)
DihedralWeightOne100Modularity (Wiles, Taylor–Wiles) (10)
GroupCohomology100Modularity (Wiles, Taylor–Wiles) (10)
Subring100Modularity (Wiles, Taylor–Wiles) (7), Level lowering (Ribet) (3)
AffineDilatation90Level lowering (Ribet) (9)
KatzModularForm90Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (9)
Valued90Level lowering (Ribet) (8), Modularity (Wiles, Taylor–Wiles) (1)
HahnSeries80Level lowering (Ribet) (4), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4)
HeckeIntegralSeam80Modularity (Wiles, Taylor–Wiles) (8)
KaehlerDifferential80Level lowering (Ribet) (4), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
LevelRaising80Level lowering (Ribet) (8)
M4aLocalCFT80Modularity (Wiles, Taylor–Wiles) (8)
PrimeSpectrum80Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (5), Level lowering (Ribet) (2)
RibetIrr80Modularity (Wiles, Taylor–Wiles) (8)
TensorProduct80Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4), Level lowering (Ribet) (2)
IsNoetherianRing70Level lowering (Ribet) (4), Modularity (Wiles, Taylor–Wiles) (2)
MonoidAlgebra70Modularity (Wiles, Taylor–Wiles) (6), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
Rat70Level lowering (Ribet) (7)
TaylorWiles70Modularity (Wiles, Taylor–Wiles) (7)
AddMonoidAlgebra60Level lowering (Ribet) (5), Modularity (Wiles, Taylor–Wiles) (1)
IsAlgClosed60Level lowering (Ribet) (3), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
IsGalois60Modularity (Wiles, Taylor–Wiles) (6)
IsLocalization60Level lowering (Ribet) (3), Modularity (Wiles, Taylor–Wiles) (3)
LocalParametrix60Modularity (Wiles, Taylor–Wiles) (6)
Localization60Level lowering (Ribet) (4), Modularity (Wiles, Taylor–Wiles) (2)
MazurAdmissible60Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (6)
Nat60Level lowering (Ribet) (4), Modularity (Wiles, Taylor–Wiles) (1)
Real60Modularity (Wiles, Taylor–Wiles) (6)
integralClosure60Modularity (Wiles, Taylor–Wiles) (4), Level lowering (Ribet) (2)
AdelicDock50Modularity (Wiles, Taylor–Wiles) (5)
AlgEquiv50Modularity (Wiles, Taylor–Wiles) (4), Level lowering (Ribet) (1)
CoherentBaseChange50Level lowering (Ribet) (4), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
CuspFormClass50Modularity (Wiles, Taylor–Wiles) (3), Level lowering (Ribet) (2)
EisensteinWeightOne50Modularity (Wiles, Taylor–Wiles) (5)
FinFlatHopf50Modularity (Wiles, Taylor–Wiles) (5)
FreyCurve51Level lowering (Ribet) (5)
Int50Level lowering (Ribet) (3), Modularity (Wiles, Taylor–Wiles) (1)
IsGaloisGroup50Modularity (Wiles, Taylor–Wiles) (5)
IsIntegral50Level lowering (Ribet) (3), Modularity (Wiles, Taylor–Wiles) (2)
IsLocalizedModule50Level lowering (Ribet) (5)
IsReduced50Level lowering (Ribet) (2), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
KummerO50Modularity (Wiles, Taylor–Wiles) (5)
M4aKummer50Modularity (Wiles, Taylor–Wiles) (5)
ModularGroup50Modularity (Wiles, Taylor–Wiles) (3), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
Pencil50Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (5)
QuadraticForm50Level lowering (Ribet) (5)
RingTheory50Modularity (Wiles, Taylor–Wiles) (3), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
SchwartzMap50Modularity (Wiles, Taylor–Wiles) (5)
TWNum50Modularity (Wiles, Taylor–Wiles) (5)
TraceFibrePushforward50Modularity (Wiles, Taylor–Wiles) (5)
V3Glue50Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4), Level lowering (Ribet) (1)
exteriorPower50Level lowering (Ribet) (5)
AnalyticOnNhd40Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4)
BialgHom40Modularity (Wiles, Taylor–Wiles) (3), Level lowering (Ribet) (1)
CommRing40Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2), Level lowering (Ribet) (1)
DirichletCharacter40Modularity (Wiles, Taylor–Wiles) (4)
FiniteField40Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2), Modularity (Wiles, Taylor–Wiles) (2)
Finsupp40Level lowering (Ribet) (2), Modularity (Wiles, Taylor–Wiles) (2)
Function40Modularity (Wiles, Taylor–Wiles) (3), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
Height40Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (4)
KummerTheory40Modularity (Wiles, Taylor–Wiles) (4)
LSeries40Modularity (Wiles, Taylor–Wiles) (4)
LinearIndependent40Level lowering (Ribet) (3), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
Monoid40Level lowering (Ribet) (3), Modularity (Wiles, Taylor–Wiles) (1)
MulAction40Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (3), Modularity (Wiles, Taylor–Wiles) (1)
RibetLevelLowering40Level lowering (Ribet) (4)
SetLike40Level lowering (Ribet) (4)
UniqueFactorizationMonoid40Modularity (Wiles, Taylor–Wiles) (3), Level lowering (Ribet) (1)
ZLattice40Modularity (Wiles, Taylor–Wiles) (4)
AbsoluteValue30Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2), Modularity (Wiles, Taylor–Wiles) (1)
Coalgebra30Modularity (Wiles, Taylor–Wiles) (1), Level lowering (Ribet) (1)
CochainCx30Level lowering (Ribet) (3)
DixmierMalliavin30Modularity (Wiles, Taylor–Wiles) (3)
EulerProduct30Modularity (Wiles, Taylor–Wiles) (3)
Field30Level lowering (Ribet) (1), Modularity (Wiles, Taylor–Wiles) (1)
Fin30Modularity (Wiles, Taylor–Wiles) (2), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
FixedPart30Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (3)
GaloisAction30Modularity (Wiles, Taylor–Wiles) (3)
GlobalGaloisRep30Modularity (Wiles, Taylor–Wiles) (3)
HeckeTreeWalk30Modularity (Wiles, Taylor–Wiles) (3)
HomogeneousLocalization30Level lowering (Ribet) (3)
IsAddCyclic30Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2), Modularity (Wiles, Taylor–Wiles) (1)
IsLocallyConstant30Modularity (Wiles, Taylor–Wiles) (3)
IsNonarchimedean30Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (3)
LaurentPolynomial30Modularity (Wiles, Taylor–Wiles) (1), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
LocalGroupLaw30Level lowering (Ribet) (3)
Manifold30Modularity (Wiles, Taylor–Wiles) (2), Level lowering (Ribet) (1)
MellinParseval30Modularity (Wiles, Taylor–Wiles) (3)
QuotSMulTop30Modularity (Wiles, Taylor–Wiles) (3)
RatFunc30Modularity (Wiles, Taylor–Wiles) (2), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
UnipotentTermUnfolding30Modularity (Wiles, Taylor–Wiles) (3)
Valuation30Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2), Level lowering (Ribet) (1)
ValuationRing30Modularity (Wiles, Taylor–Wiles) (1), Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
AddChar20Level lowering (Ribet) (1), Modularity (Wiles, Taylor–Wiles) (1)
BrauerNesbitt20Modularity (Wiles, Taylor–Wiles) (2)
CharacterModule20Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
ClassFunction20Modularity (Wiles, Taylor–Wiles) (2)
CoalgHom20Level lowering (Ribet) (2)
CommGroup20Level lowering (Ribet) (1), Modularity (Wiles, Taylor–Wiles) (1)
CommRingCat20Level lowering (Ribet) (2)
ContinuousMap20Modularity (Wiles, Taylor–Wiles) (2)
DoubleCoset20Modularity (Wiles, Taylor–Wiles) (2)
DualAssembly20Modularity (Wiles, Taylor–Wiles) (2)
Finite20Modularity (Wiles, Taylor–Wiles) (2)
Finset20Modularity (Wiles, Taylor–Wiles) (1), Level lowering (Ribet) (1)
FixedPoints20Modularity (Wiles, Taylor–Wiles) (2)
GaloisLattice20Modularity (Wiles, Taylor–Wiles) (2)
HeightOneSpectrum20Modularity (Wiles, Taylor–Wiles) (2)
HomogeneousIdeal20Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1), Level lowering (Ribet) (1)
IsBaseChange20Level lowering (Ribet) (2)
IsFractionRing20Modularity (Wiles, Taylor–Wiles) (2)
LinearEquiv20Modularity (Wiles, Taylor–Wiles) (1), Level lowering (Ribet) (1)
MWFL20Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
MazurRapoportAppendix20Level lowering (Ribet) (2)
MulSemiringAction20Modularity (Wiles, Taylor–Wiles) (2)
Multiset20Modularity (Wiles, Taylor–Wiles) (2)
PresheafOfModules20Level lowering (Ribet) (2)
RSCarrier20Modularity (Wiles, Taylor–Wiles) (2)
RatIdele20Modularity (Wiles, Taylor–Wiles) (2)
RationalLattice20Modularity (Wiles, Taylor–Wiles) (2)
RepTheory20Modularity (Wiles, Taylor–Wiles) (2)
RingEquiv20Modularity (Wiles, Taylor–Wiles) (1), Level lowering (Ribet) (1)
SlashInvariantForm20Modularity (Wiles, Taylor–Wiles) (2)
Subfield20Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1), Level lowering (Ribet) (1)
SubtractionMonoid20Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (2)
TrivSqZeroExt20Level lowering (Ribet) (2)
UnipotentTermCuspBound20Modularity (Wiles, Taylor–Wiles) (2)
VectorFourier20Modularity (Wiles, Taylor–Wiles) (2)
WRay20Modularity (Wiles, Taylor–Wiles) (2)
WhittakerBlock20Modularity (Wiles, Taylor–Wiles) (2)
AddAut10Level lowering (Ribet) (1)
AddCircle10Modularity (Wiles, Taylor–Wiles) (1)
AddEquiv10Level lowering (Ribet) (1)
AddTorsor10Level lowering (Ribet) (1)
AnnulusSlope10Level lowering (Ribet) (1)
ArithFrob10Modularity (Wiles, Taylor–Wiles) (1)
ArithFrobResidue10Modularity (Wiles, Taylor–Wiles) (1)
ArithmeticFunction10Modularity (Wiles, Taylor–Wiles) (1)
Associated10Modularity (Wiles, Taylor–Wiles) (1)
AxisWitness10Modularity (Wiles, Taylor–Wiles) (1)
BostonLenstraRibet10Level lowering (Ribet) (1)
BrauerInduction10Modularity (Wiles, Taylor–Wiles) (1)
ClassGroup10Modularity (Wiles, Taylor–Wiles) (1)
CompleteOrthogonalIdempotents10Level lowering (Ribet) (1)
ContDiff10Modularity (Wiles, Taylor–Wiles) (1)
CyclicPowerRelations10Modularity (Wiles, Taylor–Wiles) (1)
Deep10Modularity (Wiles, Taylor–Wiles) (1)
Derivation10Modularity (Wiles, Taylor–Wiles) (1)
DirectSum10Level lowering (Ribet) (1)
E34D10Modularity (Wiles, Taylor–Wiles) (1)
ENat10Level lowering (Ribet) (1)
Equiv10Level lowering (Ribet) (1)
FormalHecke10Modularity (Wiles, Taylor–Wiles) (1)
GL2F310Modularity (Wiles, Taylor–Wiles) (1)
GaussProlongation10Level lowering (Ribet) (1)
GradedAlgebra10Level lowering (Ribet) (1)
HeckeCosets10Modularity (Wiles, Taylor–Wiles) (1)
HexagonalLattice10Level lowering (Ribet) (1)
Homeomorph10Modularity (Wiles, Taylor–Wiles) (1)
IncidenceSystem10Level lowering (Ribet) (1)
InertiaOrderTransport10Modularity (Wiles, Taylor–Wiles) (1)
InnerProductSpace10Modularity (Wiles, Taylor–Wiles) (1)
IntegralClosure10Modularity (Wiles, Taylor–Wiles) (1)
IrreducibleSpace10Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
IsAdjoinRoot10Modularity (Wiles, Taylor–Wiles) (1)
IsAlgebraic10Level lowering (Ribet) (1)
IsConstructible10Level lowering (Ribet) (1)
IsDomain10Modularity (Wiles, Taylor–Wiles) (1)
IsFreeGroup10Modularity (Wiles, Taylor–Wiles) (1)
IsIntegralClosure10Level lowering (Ribet) (1)
IsIntegrallyClosedIn10Level lowering (Ribet) (1)
IsIrreducible10Modularity (Wiles, Taylor–Wiles) (1)
IsLocalHom10Modularity (Wiles, Taylor–Wiles) (1)
IsOpen10Level lowering (Ribet) (1)
IsPreconnected10Level lowering (Ribet) (1)
IsProartinian10Modularity (Wiles, Taylor–Wiles) (1)
IsRegularRing10Modularity (Wiles, Taylor–Wiles) (1)
IsSMulRegular10Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
IsSeparable10Modularity (Wiles, Taylor–Wiles) (1)
LinearAlgebra10Modularity (Wiles, Taylor–Wiles) (1)
LocalizedModule10Level lowering (Ribet) (1)
M4aTorus10Modularity (Wiles, Taylor–Wiles) (1)
MeanSquare10Modularity (Wiles, Taylor–Wiles) (1)
MellinPaleyWiener10Modularity (Wiles, Taylor–Wiles) (1)
MeromorphicAt10Modularity (Wiles, Taylor–Wiles) (1)
ModularFunction10Level lowering (Ribet) (1)
NeronSpecialFibreInfra10Level lowering (Ribet) (1)
Orthonormal10Modularity (Wiles, Taylor–Wiles) (1)
P2mOS10Level lowering (Ribet) (1)
PadicGaloisModule10Modularity (Wiles, Taylor–Wiles) (1)
PartialDeriv10Modularity (Wiles, Taylor–Wiles) (1)
PhragmenLindelof10Modularity (Wiles, Taylor–Wiles) (1)
QuotientGroup10Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
RatAdele10Modularity (Wiles, Taylor–Wiles) (1)
RepresentationTheory10Modularity (Wiles, Taylor–Wiles) (1)
RestrictedProduct10Modularity (Wiles, Taylor–Wiles) (1)
Ring10Modularity (Wiles, Taylor–Wiles) (1)
Set10Modularity (Wiles, Taylor–Wiles) (1)
SimpleGraph10Level lowering (Ribet) (1)
Sobolev10Modularity (Wiles, Taylor–Wiles) (1)
StructureConstants10Modularity (Wiles, Taylor–Wiles) (1)
Summable10Modularity (Wiles, Taylor–Wiles) (1)
TW1210Modularity (Wiles, Taylor–Wiles) (1)
TW12CD1Dock10Modularity (Wiles, Taylor–Wiles) (1)
TWLoc10Modularity (Wiles, Taylor–Wiles) (1)
TestFunctionAction10Modularity (Wiles, Taylor–Wiles) (1)
TopCat10Level lowering (Ribet) (1)
TopologicalSpace10Level lowering (Ribet) (1)
Topology10Level lowering (Ribet) (1)
Transcendental10Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly) (1)
TransportGlue10Modularity (Wiles, Taylor–Wiles) (1)
Tuple10Level lowering (Ribet) (1)
UnitAddTorus10Modularity (Wiles, Taylor–Wiles) (1)
WeightedMultigraph10Modularity (Wiles, Taylor–Wiles) (1)
WindowMultiplicity10Modularity (Wiles, Taylor–Wiles) (1)
ZSpan10Modularity (Wiles, Taylor–Wiles) (1)
minpoly10Modularity (Wiles, Taylor–Wiles) (1)