The 1,450 definition modules
Ordinary Lean files declaring the structures, predicates and instances the statements are phrased in (Frey packages, Galois representations attached to curves, modularity predicates, modular curves, automorphic forms, deformation data, …). Grouped by the first component of the file name; within a group, the modules most used by theorem statements come first. The modules named in the route documents:
Definitions/Def_EllipticCurve_ZeroComponentAt.leanstatements of 43 theoremsDefinitions/Def_FLTPrelim_CofixedLine.leanstatements of 17 theoremsDefinitions/Def_FLTPrelim_FreyPackage.leanstatements of 97 theoremsDefinitions/Def_FLTPrelim_GaloisRep.leanstatements of 174 theoremsDefinitions/Def_FLTPrelim_ModularRep.leanstatements of 119 theoremsDefinitions/Def_FLTPrelim_Modularity.leanstatements of 298 theoremsDefinitions/Def_FreyPackage_IsConductorLevel.leanstatements of 4 theoremsDefinitions/Def_WeierstrassCurve_Mlc1RowStatement.leanstatements of 2 theorems
ModularCurve 291 · AlgebraicGeometry 172 · AutomorphicForm 106 · LanglandsTunnell 84 · CerednikDrinfeld 83 · AlgebraicCurve 72 · WeierstrassCurve 61 · GroupCohomology 49 · NumberField 46 · Mathlib 42 · CuspForm 32 · GaloisRep 24 · MvFormalGroup 19 · Deformations 18 · FreyPackage 17 · TateCurve 15 · HopfAlgebra 14 · M4aHerbrand 13 · GoodReductionJacobian 12 · EllipticCurve 11 · CohCarrier 10 · Dieudonne 10 · LocalLanglands 9 · PDivisibleGroup 9 · RepTheory 9 · ExtCitation 8 · DedekindDomain 7 · QuaternionAlgebra 7 · FLTPrelim 6 · LocalNewvector 6 · ValuationSubring 6 · DrinfeldCurve 5 · ModularForm 5 · MvPolynomial 5 · FormalGroup 4 · FrobeniusDensity 4 · HeckeEis 4 · NeronModelInfra 4 · Algebra 3 · ArtinL 3 · FiniteFlat 3 · FullLevelTate 3 · HaarMeasure 3 · HeckeGalois 3 · IsDedekindDomain 3 · LaurentSeries 3 · PresheafOfModules 3 · CategoryTheory 2 · ClassGroup 2 · EisensteinGeneral 2 · EisensteinSeries 2 · ExtEndgame 2 · FieldTheory 2 · HahnSeries 2 · HeckeModule 2 · MeasureTheory 2 · NumberTheory 2 · PadicAlgCl 2 · PadicComplex 2 · Patching 2 · RibetLevelLowering 2 · SheafOfModules 2 · Submodule 2 · TaylorWiles 2 · UnramifiedWhittaker 2 · AbstractHeckeOperator 1 · AdelicDock 1 · AdicCompletionGaloisAction 1 · AdicCompletionLocalRing 1 · AdicCompletionRestrictScalars 1 · AdicCompletionRingFunctoriality 1 · AdicCompletionTensorRing 1 · Analysis 1 · ArithFrobResidue 1 · ClassFunction 1 · Compat 1 · CompletionInvariants 1 · CuspidalType 1 · CyclotomicUniv 1 · Deformation 1 · DifferentFiltrationFormula 1 · DifferentFiltrationMonogenicDischarge 1 · DirichletCharacter 1 · DualIsogenyAPI 1 · DualIsogenyExistence 1 · DualSelmer 1 · FormalHecke 1 · FreyCurve 1 · Gamma0Away 1 · Gamma0AwayUnitsChar 1 · Gamma0CoeffCohomology 1 · Gamma0CoeffCohomologyEigen 1 · Gamma0HeckeOperatorHom 1 · Gamma0UnitsChar 1 · HaarQuotient 1 · HeckeCharacter 1 · IharaAmalgam 1 · IharaAmalgamMap 1 · IharaGamma0Fin 1 · IharaIota 1 · IharaLemma 1 · IharaMennickeCarrier 1 · IncidenceSystem 1 · IntMatrixOrder 1 · InvariantBaseChange 1 · InvariantsCompletion 1 · IsLocalRing 1 · Isogeny 1 · JPSS 1 · JacJ1 1 · JacJ1Iface 1 · LatticeTreeBaseChange 1 · LatticeTreeOrbital 1 · LinearMap 1 · LocalGL2 1 · LocalReciprocity 1 · LocalRing 1 · M4aLocalCFT 1 · MDivRepresents 1 · MazurAdmissible 1 · ModPForms 1 · ModelTransfer 1 · Module 1 · MvPowerSeries 1 · NarrowRayClassGroup 1 · Nat 1 · NetPairing 1 · NormIndex 1 · PadicInt 1 · PeriodPair 1 · Polynomial 1 · PolynomialCompletion 1 · PowerSeries 1 · PrimeNormIndex 1 · ProjectiveLineMatrixAction 1 · RamificationChain 1 · RatIdele 1 · Rep 1 · Representation 1 · RingTheory 1 · SchurMultiplierTrivial 1 · SemilocalAdicCompletion 1 · SmoothOfClosedPoints 1 · StabilizerCompletionAction 1 · Stickelberger 1 · SwdAlgebra 1 · SymmetricPowerBlockwiseFTSym 1 · SymmetricPowerPowerSeriesFTSym 1 · TensorProductDomain 1 · TwistedNormClasses 1 · TwistedUnipotentTerm 1 · TwoChartCech 1 · Valuation 1
ModularCurve 291 modules
Def_ModularCurve_X1219 lines · statements of 1,419 theoremsDef_ModularCurve_SupersingularModuli35 lines · statements of 1,020 theoremsDef_ModularCurve_SupersingularNodePlaces132 lines · statements of 999 theoremsDef_ModularCurve_ArithmeticGalois141 lines · statements of 922 theoremsDef_ModularCurve_JqCoeff84 lines · statements of 901 theoremsDef_ModularCurve_FullLevelJacobian422 lines · statements of 875 theoremsDef_ModularCurve_FullLevelSemistableCovering125 lines · statements of 738 theoremsDef_ModularCurve_FullLevelLevelAutAt44 lines · statements of 639 theoremsDef_ModularCurve_UVCrossingModel115 lines · statements of 624 theoremsDef_ModularCurve_XHDRModelAtP336 lines · statements of 470 theoremsDef_ModularCurve_JHNeronObjectAtP241 lines · statements of 468 theoremsDef_ModularCurve_PlaceWidthChar116 lines · statements of 450 theoremsDef_ModularCurve_XH180 lines · statements of 375 theoremsDef_ModularCurve_HeckeModule123 lines · statements of 372 theoremsDef_ModularCurve_FullLevelSemistableCoveringW2112 lines · statements of 368 theoremsDef_ModularCurve_WeierstrassGamma0Pow107 lines · statements of 362 theoremsDef_ModularCurve_WeierstrassLevelModuliDatum113 lines · statements of 341 theoremsDef_ModularCurve_ProlongationTuple313 lines · statements of 328 theoremsDef_ModularCurve_X0349 lines · statements of 325 theoremsDef_ModularCurve_LevelModuliPackage128 lines · statements of 310 theoremsDef_ModularCurve_LevelModuliPackageAbs43 lines · statements of 307 theoremsDef_ModularCurve_TwoChartModel300 lines · statements of 297 theoremsDef_ModularCurve_WeierstrassLevelComponents208 lines · statements of 280 theoremsDef_ModularCurve_LevelRelabelling87 lines · statements of 259 theoremsDef_ModularCurve_LaurentCoeff145 lines · statements of 251 theoremsDef_ModularCurve_XHOperators134 lines · statements of 246 theoremsDef_ModularCurve_JHPlaceSpecialization259 lines · statements of 234 theoremsDef_ModularCurve_X1HeckeModule265 lines · statements of 231 theoremsDef_ModularCurve_XHDifferentialsModL469 lines · statements of 221 theoremsDef_ModularCurve_DRModelPackageLevel239 lines · statements of 208 theoremsDef_ModularCurve_ModularUnit186 lines · statements of 203 theoremsDef_ModularCurve_TateSlots191 lines · statements of 200 theoremsDef_ModularCurve_IgusaFunctionFieldX152 lines · statements of 198 theoremsDef_ModularCurve_JZeroNeronObjectAtP374 lines · statements of 191 theoremsDef_ModularCurve_CoeffSemilinearAut151 lines · statements of 182 theoremsDef_ModularCurve_CuspidalClass56 lines · statements of 180 theoremsDef_ModularCurve_KatzLevelP556 lines · statements of 177 theoremsDef_ModularCurve_GlueData127 lines · statements of 170 theoremsDef_ModularCurve_JOnePGeom30 lines · statements of 162 theoremsDef_ModularCurve_KatzLevelPCusps238 lines · statements of 161 theoremsDef_ModularCurve_WeierstrassGamma1Pow65 lines · statements of 160 theoremsDef_ModularCurve_IgusaScheme325 lines · statements of 158 theoremsDef_ModularCurve_WeierstrassH1Pow86 lines · statements of 157 theoremsDef_ModularCurve_NodeLocalizedPlaces209 lines · statements of 153 theoremsDef_ModularCurve_NodeDepth100 lines · statements of 142 theoremsDef_ModularCurve_PlaceSpecialization164 lines · statements of 137 theoremsDef_ModularCurve_JOnePOpsV241 lines · statements of 134 theoremsDef_ModularCurve_PhiGen310 lines · statements of 132 theoremsDef_ModularCurve_X0ModL157 lines · statements of 132 theoremsDef_ModularCurve_JZeroSemistableSpecialization177 lines · statements of 128 theoremsDef_ModularCurve_ReductionModL337 lines · statements of 122 theoremsDef_ModularCurve_JZeroHeightForm195 lines · statements of 118 theoremsDef_ModularCurve_PeriodMap82 lines · statements of 117 theoremsDef_ModularCurve_GenusNumerics25 lines · statements of 116 theoremsDef_ModularCurve_QExpansionDiff70 lines · statements of 111 theoremsDef_ModularCurve_DRModelPackage135 lines · statements of 109 theoremsDef_ModularCurve_JWidth47 lines · statements of 107 theoremsDef_ModularCurve_SpecializationMap4,449 lines · statements of 106 theoremsDef_ModularCurve_CharLDegeneracyHecke370 lines · statements of 103 theoremsDef_ModularCurve_ComponentGroup79 lines · statements of 103 theoremsDef_ModularCurve_NodeDescent38 lines · statements of 103 theoremsDef_ModularCurve_ModuliPlace682 lines · statements of 94 theoremsDef_ModularCurve_FullLevelSemistableCoveringGuards48 lines · statements of 87 theoremsDef_ModularCurve_NodeLocalized60 lines · statements of 87 theoremsDef_ModularCurve_SupersingularNodes97 lines · statements of 86 theoremsDef_ModularCurve_X1HeckeOperator247 lines · statements of 85 theoremsDef_ModularCurve_CharPReduction322 lines · statements of 83 theoremsDef_ModularCurve_FibreModelCuspChart31 lines · statements of 81 theoremsDef_ModularCurve_MultCoveringFamily99 lines · statements of 78 theoremsDef_ModularCurve_XHDRModelAtPCrossingFrame91 lines · statements of 78 theoremsDef_ModularCurve_DRResolvedModelPackageV4138 lines · statements of 77 theoremsDef_ModularCurve_FullLevelSemistableCoveringNaturality50 lines · statements of 72 theoremsDef_ModularCurve_LevelOneProlongationPair196 lines · statements of 69 theoremsDef_ModularCurve_HeckeOperator192 lines · statements of 68 theoremsDef_ModularCurve_SSDegeneracyHecke221 lines · statements of 68 theoremsDef_ModularCurve_GeometricBaseChange228 lines · statements of 67 theoremsDef_ModularCurve_JZeroTateModule114 lines · statements of 66 theoremsDef_ModularCurve_MultCoveringAnnuli61 lines · statements of 66 theoremsDef_ModularCurve_PlaceWidth24 lines · statements of 66 theoremsDef_ModularCurve_AtkinLehnerPartial43 lines · statements of 64 theoremsDef_ModularCurve_FibreModel105 lines · statements of 64 theoremsDef_ModularCurve_HeckeDifferential187 lines · statements of 63 theoremsDef_ModularCurve_XHHeckeOperator250 lines · statements of 62 theoremsDef_ModularCurve_QAdicPlace381 lines · statements of 61 theoremsDef_ModularCurve_X1Diamond110 lines · statements of 59 theoremsDef_ModularCurve_PeriodOf133 lines · statements of 57 theoremsDef_ModularCurve_CanonicalDivisor98 lines · statements of 56 theoremsDef_ModularCurve_X1PrimitiveSpecializationAtP92 lines · statements of 56 theoremsDef_ModularCurve_LevelOneGlueData79 lines · statements of 52 theoremsDef_ModularCurve_MazurStepThreeInputs125 lines · statements of 51 theoremsDef_ModularCurve_MultCoveringCharts237 lines · statements of 51 theoremsDef_ModularCurve_ModPFormFn35 lines · statements of 50 theoremsDef_ModularCurve_CharLSpecialFibreLevelNDictionary404 lines · statements of 49 theoremsDef_ModularCurve_ToricDescentData176 lines · statements of 47 theoremsDef_ModularCurve_PeriodLattice299 lines · statements of 45 theoremsDef_ModularCurve_WeierstrassLevelCarrier77 lines · statements of 45 theoremsDef_ModularCurve_X0MqResolvedTable44 lines · statements of 42 theoremsDef_ModularCurve_DRModelLegTwoInput112 lines · statements of 41 theoremsDef_ModularCurve_ToricMonodromyPart25 lines · statements of 41 theoremsDef_ModularCurve_DRResolvedModelPackageLevel129 lines · statements of 40 theoremsDef_ModularCurve_JZeroNeronAtPData45 lines · statements of 40 theoremsDef_ModularCurve_JZeroNeronPrimaryTorsionSheaf169 lines · statements of 40 theoremsDef_ModularCurve_SpecializeModuli204 lines · statements of 40 theoremsDef_ModularCurve_QExpReductionModL339 lines · statements of 39 theoremsDef_ModularCurve_AtkinLehner108 lines · statements of 38 theoremsDef_ModularCurve_FullLevelSemistableCoveringTelescope262 lines · statements of 38 theoremsDef_ModularCurve_HeckeProj42 lines · statements of 37 theoremsDef_ModularCurve_ComplexPlaceDictionaryOf117 lines · statements of 36 theoremsDef_ModularCurve_SSHeckeV250 lines · statements of 36 theoremsDef_ModularCurve_JZeroNeronTorsionSheafV4154 lines · statements of 35 theoremsDef_ModularCurve_ReductionOfPointsAgreesModL45 lines · statements of 35 theoremsDef_ModularCurve_CanonicalDivisorUniformizer36 lines · statements of 32 theoremsDef_ModularCurve_ComplexPlaceDictionary50 lines · statements of 32 theoremsDef_ModularCurve_EichlerShimuraData241 lines · statements of 32 theoremsDef_ModularCurve_HeckeInputsAll14 lines · statements of 32 theoremsDef_ModularCurve_JZeroNeronObjectAtP_LevelModel114 lines · statements of 32 theoremsDef_ModularCurve_SSCarrier37 lines · statements of 32 theoremsDef_ModularCurve_CharacterLatticePairings210 lines · statements of 31 theoremsDef_ModularCurve_LambdaSeries35 lines · statements of 30 theoremsDef_ModularCurve_JHNodeDepth152 lines · statements of 28 theoremsDef_ModularCurve_UVCrossingGaussOrder53 lines · statements of 28 theoremsDef_ModularCurve_DRModelPackageLevelCrossingFrame51 lines · statements of 27 theoremsDef_ModularCurve_QExpCoeffSemilinearAut281 lines · statements of 27 theoremsDef_ModularCurve_JHNodeDepthInf32 lines · statements of 26 theoremsDef_ModularCurve_ComponentGroupHecke114 lines · statements of 25 theoremsDef_ModularCurve_DegeneracyTower139 lines · statements of 25 theoremsDef_ModularCurve_JZeroNeronObjectAtP_NeronExtension161 lines · statements of 24 theoremsDef_ModularCurve_ModuliPointMap160 lines · statements of 24 theoremsDef_ModularCurve_MultCoveringLink63 lines · statements of 24 theoremsDef_ModularCurve_EtaQuotient111 lines · statements of 23 theoremsDef_ModularCurve_UVCrossingDominantIndices35 lines · statements of 23 theoremsDef_ModularCurve_XHDiamondModL51 lines · statements of 23 theoremsDef_ModularCurve_DRModelPackageCrossingFrame56 lines · statements of 22 theoremsDef_ModularCurve_JZeroNeronPrimaryTorsionFlag92 lines · statements of 21 theoremsDef_ModularCurve_CharLFrobeniusGeomLevel1,594 lines · statements of 20 theoremsDef_ModularCurve_LambdaNodeLocalized61 lines · statements of 20 theoremsDef_ModularCurve_WeierstrassGamma0Sqf95 lines · statements of 20 theoremsDef_ModularCurve_WeightDivisor40 lines · statements of 20 theoremsDef_ModularCurve_DRResolvedModelChartsLevelRam58 lines · statements of 19 theoremsDef_ModularCurve_FibrePoly54 lines · statements of 19 theoremsDef_ModularCurve_HpoolLevelRing99 lines · statements of 19 theoremsDef_ModularCurve_LevelNFunctionField54 lines · statements of 19 theoremsDef_ModularCurve_ProlongationTupleSmoothPoint84 lines · statements of 19 theoremsDef_ModularCurve_QExpSemistableSpecializationPinnedV3174 lines · statements of 19 theoremsDef_ModularCurve_TateFormal161 lines · statements of 19 theoremsDef_ModularCurve_FrobeniusModL343 lines · statements of 18 theoremsDef_ModularCurve_JOnePOpsV338 lines · statements of 18 theoremsDef_ModularCurve_LambdaNodeDescent48 lines · statements of 18 theoremsDef_ModularCurve_PeriodMapBundled31 lines · statements of 18 theoremsDef_ModularCurve_QExpSemistableSpecializationPinned222 lines · statements of 18 theoremsDef_ModularCurve_KroneckerTransport215 lines · statements of 17 theoremsDef_ModularCurve_ShimuraKernel90 lines · statements of 17 theoremsDef_ModularCurve_X1DegeneracyPullback181 lines · statements of 17 theoremsDef_ModularCurve_EMD54 lines · statements of 16 theoremsDef_ModularCurve_EisensteinTwoCoeff25 lines · statements of 16 theoremsDef_ModularCurve_JLinePlaces65 lines · statements of 16 theoremsDef_ModularCurve_JZeroNeronIdentityComponent68 lines · statements of 16 theoremsDef_ModularCurve_LambdaModularPolynomialData21 lines · statements of 16 theoremsDef_ModularCurve_ModuliPoint163 lines · statements of 16 theoremsDef_ModularCurve_FullLevelSemistableCoveringInertiaIgusa32 lines · statements of 15 theoremsDef_ModularCurve_JZeroHeightFormPositivity107 lines · statements of 15 theoremsDef_ModularCurve_JHTwistType77 lines · statements of 14 theoremsDef_ModularCurve_LegendreJ11 lines · statements of 14 theoremsDef_ModularCurve_LevelOneProlongationPairRegularity50 lines · statements of 14 theoremsDef_ModularCurve_MazurPrincipleCore69 lines · statements of 14 theoremsDef_ModularCurve_RigidDescentHyps327 lines · statements of 14 theoremsDef_ModularCurve_KatzLevelPUniversal344 lines · statements of 13 theoremsDef_ModularCurve_PeriodHomPair157 lines · statements of 13 theoremsDef_ModularCurve_PrimCosetReps50 lines · statements of 13 theoremsDef_ModularCurve_QExpFrobeniusModL312 lines · statements of 13 theoremsDef_ModularCurve_SmoothPointLocalRing82 lines · statements of 13 theoremsDef_ModularCurve_AnnulusSpecializationLevel178 lines · statements of 12 theoremsDef_ModularCurve_EisensteinIdeal38 lines · statements of 12 theoremsDef_ModularCurve_MultiplicativeType16 lines · statements of 12 theoremsDef_ModularCurve_ResolvedModelSite426 lines · statements of 12 theoremsDef_ModularCurve_DRModelPackageLevelAPI236 lines · statements of 11 theoremsDef_ModularCurve_LevelOneAnnulusSpecializationOrbit181 lines · statements of 11 theoremsDef_ModularCurve_ResolvedModelSiteLevel432 lines · statements of 11 theoremsDef_ModularCurve_SiegelFunction33 lines · statements of 11 theoremsDef_ModularCurve_StepThreeDoorPredicates65 lines · statements of 11 theoremsDef_ModularCurve_CuspSpace376 lines · statements of 10 theoremsDef_ModularCurve_JZeroNaiveHeight117 lines · statements of 10 theoremsDef_ModularCurve_ChartSemicontinuity144 lines · statements of 9 theoremsDef_ModularCurve_DegeneracyVp150 lines · statements of 9 theoremsDef_ModularCurve_JHTwistedDatum107 lines · statements of 9 theoremsDef_ModularCurve_JZeroToricTorsion27 lines · statements of 9 theoremsDef_ModularCurve_SmoothedFundamental188 lines · statements of 9 theoremsDef_ModularCurve_CycSubRootBridgeN169 lines · statements of 8 theoremsDef_ModularCurve_DRResolvedModelCharts56 lines · statements of 8 theoremsDef_ModularCurve_HeckeOperatorModL69 lines · statements of 8 theoremsDef_ModularCurve_PDPairing672 lines · statements of 8 theoremsDef_ModularCurve_SpecialisationVocab144 lines · statements of 8 theoremsDef_ModularCurve_UVCrossingChart49 lines · statements of 8 theoremsDef_ModularCurve_ComponentGroupKirchhoff166 lines · statements of 7 theoremsDef_ModularCurve_CupPairing47 lines · statements of 7 theoremsDef_ModularCurve_EichlerMass17 lines · statements of 7 theoremsDef_ModularCurve_FinitePlaceLift538 lines · statements of 7 theoremsDef_ModularCurve_FullLevelCuspidalSpecialization135 lines · statements of 7 theoremsDef_ModularCurve_TatePoint112 lines · statements of 7 theoremsDef_ModularCurve_UVCrossingInitialForm61 lines · statements of 7 theoremsDef_ModularCurve_AttachmentConcrete26 lines · statements of 6 theoremsDef_ModularCurve_ClassicalModularPolynomials46 lines · statements of 6 theoremsDef_ModularCurve_DRModelLegTwoInputV265 lines · statements of 6 theoremsDef_ModularCurve_HeckeOperatorTotal55 lines · statements of 6 theoremsDef_ModularCurve_JHCuspChartSet29 lines · statements of 6 theoremsDef_ModularCurve_JZeroGoodReductionV286 lines · statements of 6 theoremsDef_ModularCurve_JZeroNeronData144 lines · statements of 6 theoremsDef_ModularCurve_LevelOneChartFst394 lines · statements of 6 theoremsDef_ModularCurve_ToricDichotomyData62 lines · statements of 6 theoremsDef_ModularCurve_AutomorphicField203 lines · statements of 5 theoremsDef_ModularCurve_EigenformIdeal25 lines · statements of 5 theoremsDef_ModularCurve_JHChartSemicontinuity59 lines · statements of 5 theoremsDef_ModularCurve_JOnePOps40 lines · statements of 5 theoremsDef_ModularCurve_JZeroNeronAtPDataOrdV2227 lines · statements of 5 theoremsDef_ModularCurve_JZeroNeronIdentityComponentGood76 lines · statements of 5 theoremsDef_ModularCurve_JZeroTorsionFinite28 lines · statements of 5 theoremsDef_ModularCurve_KatzLevelPQuotient120 lines · statements of 5 theoremsDef_ModularCurve_QAdicPlaceMod364 lines · statements of 5 theoremsDef_ModularCurve_Eisenstein40 lines · statements of 4 theoremsDef_ModularCurve_JZeroNeronTorsionFlag95 lines · statements of 4 theoremsDef_ModularCurve_ModularEquationQ65 lines · statements of 4 theoremsDef_ModularCurve_SL2Elementary75 lines · statements of 4 theoremsDef_ModularCurve_SpecialisationBridge291 lines · statements of 4 theoremsDef_ModularCurve_HahnSpecialise327 lines · statements of 3 theoremsDef_ModularCurve_HeckeNamedInputs59 lines · statements of 3 theoremsDef_ModularCurve_IgusaFunctionField77 lines · statements of 3 theoremsDef_ModularCurve_LevelOneAnnulusSpecialization143 lines · statements of 3 theoremsDef_ModularCurve_LevelOneProlongationPairSplit91 lines · statements of 3 theoremsDef_ModularCurve_NodeLocalizedPresentation155 lines · statements of 3 theoremsDef_ModularCurve_PeriodTransfer151 lines · statements of 3 theoremsDef_ModularCurve_ProlongationTuple_JumpLaw70 lines · statements of 3 theoremsDef_ModularCurve_SSCarrier342 lines · statements of 3 theoremsDef_ModularCurve_SupportTransfer52 lines · statements of 3 theoremsDef_ModularCurve_AbelFibreSumOf41 lines · statements of 2 theoremsDef_ModularCurve_DeligneRapoport43 lines · statements of 2 theoremsDef_ModularCurve_GaussPencilAdapter352 lines · statements of 2 theoremsDef_ModularCurve_JZeroGoodReductionV381 lines · statements of 2 theoremsDef_ModularCurve_JZeroNeronAtPDataCore100 lines · statements of 2 theoremsDef_ModularCurve_JZeroNeronDataPrime147 lines · statements of 2 theoremsDef_ModularCurve_KatzLevelPClassifyingMaps660 lines · statements of 2 theoremsDef_ModularCurve_LevelFunctionField206 lines · statements of 2 theoremsDef_ModularCurve_LevelNormalForm35 lines · statements of 2 theoremsDef_ModularCurve_LevelOneComp68 lines · statements of 2 theoremsDef_ModularCurve_MTorsionDiff67 lines · statements of 2 theoremsDef_ModularCurve_NodeDescentTower160 lines · statements of 2 theoremsDef_ModularCurve_PernodeConclusion149 lines · statements of 2 theoremsDef_ModularCurve_PernodeHyps175 lines · statements of 2 theoremsDef_ModularCurve_ResidualRealization55 lines · statements of 2 theoremsDef_ModularCurve_SupersingularLocus52 lines · statements of 2 theoremsDef_ModularCurve_TateOrigin54 lines · statements of 2 theoremsDef_ModularCurve_UniformizedHeckeCurve63 lines · statements of 2 theoremsDef_ModularCurve_AbelFibreSum48 lines · statements of 1 theoremsDef_ModularCurve_AtPPackage49 lines · statements of 1 theoremsDef_ModularCurve_ComponentGroupOrder53 lines · statements of 1 theoremsDef_ModularCurve_CycSubRootBridgeOdd95 lines · statements of 1 theoremsDef_ModularCurve_HeckeCarrier108 lines · statements of 1 theoremsDef_ModularCurve_JZeroOrdConn118 lines · statements of 1 theoremsDef_ModularCurve_JZeroTorsionHopfOrder62 lines · statements of 1 theoremsDef_ModularCurve_OmegaOf95 lines · statements of 1 theoremsDef_ModularCurve_ProjectiveLine94 lines · statements of 1 theoremsDef_ModularCurve_RigidDescentNodesConclusion192 lines · statements of 1 theoremsDef_ModularCurve_ShimuraCovering136 lines · statements of 1 theoremsDef_ModularCurve_TateVeluRing225 lines · statements of 1 theoremsDef_ModularCurve_TateVeluRingTwo64 lines · statements of 1 theoremsDef_ModularCurve_TwoNewEigenformIdeal23 lines · statements of 1 theoremsDef_ModularCurve_CharLFrobeniusGeomLevelUnconditional261 lines · statements of 0 theoremsDef_ModularCurve_CharLSpecialFibrePic0CommutingFamilyBridge99 lines · statements of 0 theoremsDef_ModularCurve_CharLSpecialFibrePic0ForallMBridge127 lines · statements of 0 theoremsDef_ModularCurve_CycSubRootBridge197 lines · statements of 0 theoremsDef_ModularCurve_DRResolvedModelPackageLevelRam126 lines · statements of 0 theoremsDef_ModularCurve_FppfKummerInterface60 lines · statements of 0 theoremsDef_ModularCurve_HeckeAlgebraHom115 lines · statements of 0 theoremsDef_ModularCurve_HeckeSeam328 lines · statements of 0 theoremsDef_ModularCurve_JLinePlacesBar67 lines · statements of 0 theoremsDef_ModularCurve_JZeroNeronAtPDataOrdCore23 lines · statements of 0 theoremsDef_ModularCurve_JZeroNeronAtPDataSameIdeal28 lines · statements of 0 theoremsDef_ModularCurve_KatzBaseChange206 lines · statements of 0 theoremsDef_ModularCurve_KatzLevelPTorusPairs266 lines · statements of 0 theoremsDef_ModularCurve_KatzLevelPYoneda407 lines · statements of 0 theoremsDef_ModularCurve_KwNo6HspecCartierDlogCampaignFrame222 lines · statements of 0 theoremsDef_ModularCurve_LaurentBaseChangeTower60 lines · statements of 0 theoremsDef_ModularCurve_LaurentDescent172 lines · statements of 0 theoremsDef_ModularCurve_LevelBaseRing277 lines · statements of 0 theoremsDef_ModularCurve_LevelOneProlongationPairSplitEff42 lines · statements of 0 theoremsDef_ModularCurve_MazurStepThree24 lines · statements of 0 theoremsDef_ModularCurve_QAdicPlaceModV287 lines · statements of 0 theoremsDef_ModularCurve_RouteBCoordRing37 lines · statements of 0 theoremsDef_ModularCurve_ShimuraGenerator186 lines · statements of 0 theoremsDef_ModularCurve_ShimuraSubgroup58 lines · statements of 0 theoremsDef_ModularCurve_SpecializationWitness101 lines · statements of 0 theoremsDef_ModularCurve_X1PrimitiveSpecialization97 lines · statements of 0 theorems
AlgebraicGeometry 172 modules
Def_AlgebraicGeometry_RelativePicardFunctor182 lines · statements of 1,507 theoremsDef_AlgebraicGeometry_RelPicardAlgEquivZeroCut121 lines · statements of 908 theoremsDef_AlgebraicGeometry_RepresentsRelSubPic74 lines · statements of 796 theoremsDef_AlgebraicGeometry_RelativeGroupLaw194 lines · statements of 699 theoremsDef_AlgebraicGeometry_IdealSheafModule45 lines · statements of 594 theoremsDef_AlgebraicGeometry_SmoothProperCurveBase89 lines · statements of 580 theoremsDef_AlgebraicGeometry_RelEffCartierDiv201 lines · statements of 551 theoremsDef_AlgebraicGeometry_RelPicardAlgEquivZeroGroupCut147 lines · statements of 548 theoremsDef_AlgebraicGeometry_NeronModelPropertyBundleCarrier326 lines · statements of 536 theoremsDef_AlgebraicGeometry_NeronModelEndomorphismExtension335 lines · statements of 528 theoremsDef_AlgebraicGeometry_TwoAffineOpenCover130 lines · statements of 491 theoremsDef_AlgebraicGeometry_RelativePic0DesignationBaseChange42 lines · statements of 487 theoremsDef_AlgebraicGeometry_RelEffCartierDivOfPoint83 lines · statements of 452 theoremsDef_AlgebraicGeometry_RelSubPicBaseChange300 lines · statements of 433 theoremsDef_AlgebraicGeometry_PolarisationRosati71 lines · statements of 399 theoremsDef_AlgebraicGeometry_RelPicardPullback152 lines · statements of 370 theoremsDef_AlgebraicGeometry_RelSubPicGroup250 lines · statements of 329 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCech251 lines · statements of 310 theoremsDef_AlgebraicGeometry_TwoChartCechSectionsOf81 lines · statements of 301 theoremsDef_AlgebraicGeometry_ModulesRigidify34 lines · statements of 296 theoremsDef_AlgebraicGeometry_PolarisedAbelianScheme126 lines · statements of 254 theoremsDef_AlgebraicGeometry_ProjSpace453 lines · statements of 225 theoremsDef_AlgebraicGeometry_OrderedAffineCoverComap113 lines · statements of 185 theoremsDef_AlgebraicGeometry_RelPicardThetaBundle43 lines · statements of 156 theoremsDef_AlgebraicGeometry_OModulePresheafOfModules59 lines · statements of 151 theoremsDef_AlgebraicGeometry_OModulePresheafHom214 lines · statements of 147 theoremsDef_AlgebraicGeometry_ModulesTensorPowV229 lines · statements of 140 theoremsDef_AlgebraicGeometry_RelPicardChartSections47 lines · statements of 122 theoremsDef_AlgebraicGeometry_ModulesProjPresentation117 lines · statements of 119 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCochainPullback73 lines · statements of 114 theoremsDef_AlgebraicGeometry_ModulesSectionZeroScheme113 lines · statements of 108 theoremsDef_AlgebraicGeometry_SmallExtensionPairTangent59 lines · statements of 108 theoremsDef_AlgebraicGeometry_SmallExtensionTangentCoords58 lines · statements of 103 theoremsDef_AlgebraicGeometry_ModulesSectionsTensor254 lines · statements of 99 theoremsDef_AlgebraicGeometry_SmoothProperCurveFiniteMapData129 lines · statements of 99 theoremsDef_AlgebraicGeometry_ModulesNormModule65 lines · statements of 98 theoremsDef_AlgebraicGeometry_OModulePresheafEulerChar35 lines · statements of 98 theoremsDef_AlgebraicGeometry_PolarisationPicZero26 lines · statements of 88 theoremsDef_AlgebraicGeometry_RiemannForm72 lines · statements of 87 theoremsDef_AlgebraicGeometry_TangentCoordsOfPairAt46 lines · statements of 84 theoremsDef_AlgebraicGeometry_SquareZeroDeformation154 lines · statements of 82 theoremsDef_AlgebraicGeometry_RelativeGroupLawEndDegree116 lines · statements of 81 theoremsDef_AlgebraicGeometry_SquareZeroRelTangent77 lines · statements of 76 theoremsDef_AlgebraicGeometry_TangentCoordsOfPair153 lines · statements of 74 theoremsDef_AlgebraicGeometry_HilbertFunctor38 lines · statements of 68 theoremsDef_AlgebraicGeometry_RelEffCartierDivSupportedIn128 lines · statements of 66 theoremsDef_AlgebraicGeometry_ModulesTensorPow20 lines · statements of 63 theoremsDef_AlgebraicGeometry_FramedPolarisedAbelianScheme91 lines · statements of 62 theoremsDef_AlgebraicGeometry_TwoChartCech257 lines · statements of 56 theoremsDef_AlgebraicGeometry_ModulesPullbackLocalSection109 lines · statements of 55 theoremsDef_AlgebraicGeometry_PolarisedAbelianSchemeOfType121 lines · statements of 51 theoremsDef_AlgebraicGeometry_TwoAffineOpenCoverKaehler452 lines · statements of 51 theoremsDef_AlgebraicGeometry_ModulesSectionsTensorV253 lines · statements of 50 theoremsDef_AlgebraicGeometry_ModulesDet32 lines · statements of 49 theoremsDef_AlgebraicGeometry_RelSubPicPresheaf158 lines · statements of 47 theoremsDef_AlgebraicGeometry_CechPicardObstruction112 lines · statements of 46 theoremsDef_AlgebraicGeometry_ThetaAdaptedFrame48 lines · statements of 46 theoremsDef_AlgebraicGeometry_OModulePresheafConstructions344 lines · statements of 44 theoremsDef_AlgebraicGeometry_ProjTwistDatum591 lines · statements of 43 theoremsDef_AlgebraicGeometry_ModulesSectionZeroSchemeV224 lines · statements of 42 theoremsDef_AlgebraicGeometry_RelEffCartierDivSum184 lines · statements of 42 theoremsDef_AlgebraicGeometry_FormalGroupAlongSection57 lines · statements of 40 theoremsDef_AlgebraicGeometry_FppfSiteCohomology303 lines · statements of 40 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCechCup61 lines · statements of 38 theoremsDef_AlgebraicGeometry_SplitTorusMu76 lines · statements of 38 theoremsDef_AlgebraicGeometry_RigidifiedLineBundleOfInvertible142 lines · statements of 37 theoremsDef_AlgebraicGeometry_ProjSpaceCover71 lines · statements of 36 theoremsDef_AlgebraicGeometry_DoubleComplex231 lines · statements of 35 theoremsDef_AlgebraicGeometry_ModulesLocallyFreeOfRank18 lines · statements of 35 theoremsDef_AlgebraicGeometry_TowerQuotientDatum81 lines · statements of 34 theoremsDef_AlgebraicGeometry_KaehlerModule110 lines · statements of 33 theoremsDef_AlgebraicGeometry_ThetaGroupLaw372 lines · statements of 33 theoremsDef_AlgebraicGeometry_RelEffCartierDivFunctor192 lines · statements of 31 theoremsDef_AlgebraicGeometry_RelEffCartierDivTwist238 lines · statements of 29 theoremsDef_AlgebraicGeometry_ModulesPullbackMonoidal84 lines · statements of 28 theoremsDef_AlgebraicGeometry_AffineLimit58 lines · statements of 27 theoremsDef_AlgebraicGeometry_LocalRepresentabilityULift194 lines · statements of 26 theorems · adapted from upstreamDef_AlgebraicGeometry_ThetaLevelGroup271 lines · statements of 26 theoremsDef_AlgebraicGeometry_TangentCoordsOfPairAtVia42 lines · statements of 25 theoremsDef_AlgebraicGeometry_TwoGluedCurvesNodeUnitModule55 lines · statements of 25 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCechOrdered157 lines · statements of 24 theoremsDef_AlgebraicGeometry_PicDualNumberDeformationClassSpec60 lines · statements of 24 theoremsDef_AlgebraicGeometry_ProjSpaceCechTwist168 lines · statements of 23 theoremsDef_AlgebraicGeometry_ProjSpaceCechGradedModule749 lines · statements of 22 theoremsDef_AlgebraicGeometry_RelEffCartierDivRestrict269 lines · statements of 22 theoremsDef_AlgebraicGeometry_OModulePresheafIdealFiltration284 lines · statements of 20 theoremsDef_AlgebraicGeometry_AdicThickening67 lines · statements of 19 theoremsDef_AlgebraicGeometry_TwoAffineOpenCoverH1BaseChange235 lines · statements of 19 theoremsDef_AlgebraicGeometry_DescentCharacter75 lines · statements of 18 theoremsDef_AlgebraicGeometry_RelPicardStageHom57 lines · statements of 18 theoremsDef_AlgebraicGeometry_GradedOAlgebraSectionRing60 lines · statements of 17 theoremsDef_AlgebraicGeometry_GradedOAlgebraToProj37 lines · statements of 17 theoremsDef_AlgebraicGeometry_ThetaGroup240 lines · statements of 17 theoremsDef_AlgebraicGeometry_TwoChartCechSerrePairingInt68 lines · statements of 17 theoremsDef_AlgebraicGeometry_BiCech304 lines · statements of 16 theoremsDef_AlgebraicGeometry_RigKerDualNumber136 lines · statements of 16 theoremsDef_AlgebraicGeometry_OModulePresheafCechPushforward220 lines · statements of 15 theoremsDef_AlgebraicGeometry_BoundedCochainTensor113 lines · statements of 14 theoremsDef_AlgebraicGeometry_FppfKummerProp17715 lines · statements of 14 theoremsDef_AlgebraicGeometry_OModulePresheafTensor111 lines · statements of 14 theoremsDef_AlgebraicGeometry_SchemeFrobenius210 lines · statements of 14 theoremsDef_AlgebraicGeometry_TorsionCharacter47 lines · statements of 14 theoremsDef_AlgebraicGeometry_SchemeFibreEndo28 lines · statements of 12 theoremsDef_AlgebraicGeometry_TwoAffineOpenCoverSectional55 lines · statements of 12 theoremsDef_AlgebraicGeometry_FppfCohomologyLES652 lines · statements of 11 theoremsDef_AlgebraicGeometry_ModulesBaseChangeHom125 lines · statements of 11 theoremsDef_AlgebraicGeometry_ThetaReframe29 lines · statements of 11 theoremsDef_AlgebraicGeometry_TwoChartCechLaurentChart294 lines · statements of 11 theoremsDef_AlgebraicGeometry_ModulesGlueOfCocycle360 lines · statements of 10 theoremsDef_AlgebraicGeometry_RelPicardAbelJacobiFamily119 lines · statements of 10 theoremsDef_AlgebraicGeometry_DescentAction544 lines · statements of 9 theoremsDef_AlgebraicGeometry_ModulesPullbackMonoidalV225 lines · statements of 9 theoremsDef_AlgebraicGeometry_OModulePresheafInternalHom164 lines · statements of 9 theoremsDef_AlgebraicGeometry_ModulesIhomSections1,105 lines · statements of 8 theoremsDef_AlgebraicGeometry_OModulePresheafLerayDoubleComplex241 lines · statements of 8 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCechOrderedChains137 lines · statements of 8 theoremsDef_AlgebraicGeometry_MumfordTruncation126 lines · statements of 6 theoremsDef_AlgebraicGeometry_SymmRootFunctor170 lines · statements of 6 theoremsDef_AlgebraicGeometry_TwoGluedProjectiveLinesNodeUnitModule61 lines · statements of 6 theoremsDef_AlgebraicGeometry_CoherentBaseChange75 lines · statements of 5 theoremsDef_AlgebraicGeometry_IdealSheafModuleMaps68 lines · statements of 5 theoremsDef_AlgebraicGeometry_IterCech350 lines · statements of 5 theoremsDef_AlgebraicGeometry_ResolvedModelGlueComponents993 lines · statements of 5 theoremsDef_AlgebraicGeometry_KwCartierOperatorTCoordEngine545 lines · statements of 4 theoremsDef_AlgebraicGeometry_MazurRapoportAppendixPicNeronCarriers496 lines · statements of 4 theoremsDef_AlgebraicGeometry_ModulesProjectionMorphism39 lines · statements of 4 theoremsDef_AlgebraicGeometry_ModulesTildePullback68 lines · statements of 4 theoremsDef_AlgebraicGeometry_OModulePresheafFamilyFramesGradedModule450 lines · statements of 4 theoremsDef_AlgebraicGeometry_OModulePresheafLerayBicomplex520 lines · statements of 4 theoremsDef_AlgebraicGeometry_ProjSpaceLinMap96 lines · statements of 4 theoremsDef_AlgebraicGeometry_RelativeGroupLawGrpObj327 lines · statements of 4 theoremsDef_AlgebraicGeometry_ThetaGroupAction72 lines · statements of 4 theoremsDef_AlgebraicGeometry_FppfAmitsurTrivial18 lines · statements of 3 theoremsDef_AlgebraicGeometry_OrderedAffineCoverCechReversal47 lines · statements of 3 theoremsDef_AlgebraicGeometry_OrderedAffineCoverOf135 lines · statements of 3 theoremsDef_AlgebraicGeometry_RigKerDualNumberBaseTransport245 lines · statements of 3 theoremsDef_AlgebraicGeometry_CoherentBaseChangeFamily24 lines · statements of 2 theoremsDef_AlgebraicGeometry_FGSubalgebra119 lines · statements of 2 theoremsDef_AlgebraicGeometry_FppfKummerCalculus481 lines · statements of 2 theoremsDef_AlgebraicGeometry_ModulesWedge216 lines · statements of 2 theoremsDef_AlgebraicGeometry_NeronSpecialFibreRestriction401 lines · statements of 2 theoremsDef_AlgebraicGeometry_OModulePresheafTensorMap164 lines · statements of 2 theoremsDef_AlgebraicGeometry_SymmRootAdm51 lines · statements of 2 theoremsDef_AlgebraicGeometry_FppfH0Identification785 lines · statements of 1 theoremsDef_AlgebraicGeometry_KwPthPowerKerDExpansionEngine300 lines · statements of 1 theoremsDef_AlgebraicGeometry_OModulePresheafSectionsLinearRes37 lines · statements of 1 theoremsDef_AlgebraicGeometry_RelSubPicGlue162 lines · statements of 1 theoremsDef_AlgebraicGeometry_SubalgebraStages189 lines · statements of 1 theoremsDef_AlgebraicGeometry_FGSubalgebraTensorStage80 lines · statements of 0 theoremsDef_AlgebraicGeometry_FppfGmRepresentable386 lines · statements of 0 theoremsDef_AlgebraicGeometry_HomogeneousIdealQuotientGradingInfra630 lines · statements of 0 theoremsDef_AlgebraicGeometry_IdealSheafHom190 lines · statements of 0 theoremsDef_AlgebraicGeometry_IdealSheafModuleV224 lines · statements of 0 theoremsDef_AlgebraicGeometry_Kmf2FiberSpecTensorStalkLeg1AffineDatum130 lines · statements of 0 theoremsDef_AlgebraicGeometry_KwCartierDlogFixednessEngine636 lines · statements of 0 theoremsDef_AlgebraicGeometry_KwFrobSemilinearFixedPointFiniteEngine188 lines · statements of 0 theoremsDef_AlgebraicGeometry_KwSmoothIrredRelDimConstantEngine398 lines · statements of 0 theoremsDef_AlgebraicGeometry_MazurRapoportAppendixGenericFibreOpenImmersionDVR196 lines · statements of 0 theoremsDef_AlgebraicGeometry_ModulesIhomSectionsV2131 lines · statements of 0 theoremsDef_AlgebraicGeometry_ModulesPushforwardRestrict54 lines · statements of 0 theoremsDef_AlgebraicGeometry_ModulesRestrictOpen152 lines · statements of 0 theoremsDef_AlgebraicGeometry_ModulesRigidifyV219 lines · statements of 0 theoremsDef_AlgebraicGeometry_NeronModelUniquenessUpToIsomorphism403 lines · statements of 0 theoremsDef_AlgebraicGeometry_ProjectiveWeierstrassPolynomialPrime393 lines · statements of 0 theoremsDef_AlgebraicGeometry_RegularLocalRingFaithfullyFlatDescent504 lines · statements of 0 theoremsDef_AlgebraicGeometry_RegularLocalRingQuotientNonZeroDivisorAscent353 lines · statements of 0 theoremsDef_AlgebraicGeometry_RegularLocalRingRegularSequenceAscent425 lines · statements of 0 theoremsDef_AlgebraicGeometry_RelSubPicGroupV2603 lines · statements of 0 theoremsDef_AlgebraicGeometry_ResolvedModelGlue939 lines · statements of 0 theoremsDef_AlgebraicGeometry_ResolvedModelGlueFibre505 lines · statements of 0 theoremsDef_AlgebraicGeometry_TwoAffineOpenCoverPreimage91 lines · statements of 0 theoremsDef_AlgebraicGeometry_TwoChartCechCupProduct78 lines · statements of 0 theorems
AutomorphicForm 106 modules
Def_AutomorphicForm_TwistedOrbital575 lines · statements of 877 theoremsDef_AutomorphicForm_LocalOrbitalBase434 lines · statements of 518 theoremsDef_AutomorphicForm_WeylIntertwining56 lines · statements of 514 theoremsDef_AutomorphicForm_SmoothAutomorphicFnAt91 lines · statements of 480 theoremsDef_AutomorphicForm_FactorizableTestFn67 lines · statements of 435 theoremsDef_AutomorphicForm_InducedSection94 lines · statements of 417 theoremsDef_AutomorphicForm_EtaFamily113 lines · statements of 407 theoremsDef_AutomorphicForm_AdelicMaximalCompact332 lines · statements of 401 theoremsDef_AutomorphicForm_TruncationOperator82 lines · statements of 401 theoremsDef_AutomorphicForm_ArchKFinite70 lines · statements of 374 theoremsDef_AutomorphicForm_CanonicalTruncationDomain72 lines · statements of 362 theoremsDef_AutomorphicForm_RightConvolution38 lines · statements of 356 theoremsDef_AutomorphicForm_ProductionPinsGeneral469 lines · statements of 326 theoremsDef_AutomorphicForm_WhittakerCoefficient62 lines · statements of 310 theoremsDef_AutomorphicForm_AdelicKernel42 lines · statements of 288 theoremsDef_AutomorphicForm_FormalBaseChange74 lines · statements of 284 theoremsDef_AutomorphicForm_CarrierPins77 lines · statements of 282 theoremsDef_AutomorphicForm_SlabProfile60 lines · statements of 279 theoremsDef_AutomorphicForm_IsotypicCuspSpace1,063 lines · statements of 271 theoremsDef_AutomorphicForm_CuspidalConstituent159 lines · statements of 263 theoremsDef_AutomorphicForm_GeometricRemainder54 lines · statements of 243 theoremsDef_AutomorphicForm_GL2ConjugacyCells55 lines · statements of 223 theoremsDef_AutomorphicForm_SmoothingKernel980 lines · statements of 207 theoremsDef_AutomorphicForm_AdelicLsXi56 lines · statements of 204 theoremsDef_AutomorphicForm_TwistedAdelicKernel30 lines · statements of 186 theoremsDef_AutomorphicForm_BaseChangePlaces438 lines · statements of 176 theoremsDef_AutomorphicForm_ConstantTerm64 lines · statements of 176 theoremsDef_AutomorphicForm_AutomorphicFnAt72 lines · statements of 173 theoremsDef_AutomorphicForm_ArchWeightChar180 lines · statements of 169 theoremsDef_AutomorphicForm_ArchDerivCasimir446 lines · statements of 159 theoremsDef_AutomorphicForm_WeightedOrbitalRelation112 lines · statements of 153 theoremsDef_AutomorphicForm_RowIsometryInvariance211 lines · statements of 150 theoremsDef_AutomorphicForm_ResidualSpan32 lines · statements of 147 theoremsDef_AutomorphicForm_ArchWeightCharTransport135 lines · statements of 122 theoremsDef_AutomorphicForm_SatakeCombinationCoeff49 lines · statements of 121 theoremsDef_AutomorphicForm_SigmaAdelicAction96 lines · statements of 120 theoremsDef_AutomorphicForm_GodementSection93 lines · statements of 90 theoremsDef_AutomorphicForm_HeckeEigenfunction121 lines · statements of 87 theoremsDef_AutomorphicForm_SiegelCoordinates262 lines · statements of 86 theoremsDef_AutomorphicForm_ArchDerivCasimirComplex197 lines · statements of 79 theoremsDef_AutomorphicForm_TranslateSpanOccurrence250 lines · statements of 71 theoremsDef_AutomorphicForm_CuspidalSpectrumCarrier289 lines · statements of 70 theoremsDef_AutomorphicForm_UnipotentQuotient37 lines · statements of 68 theoremsDef_AutomorphicForm_WhittakerModelLocal65 lines · statements of 66 theoremsDef_AutomorphicForm_WindingDatum85 lines · statements of 63 theoremsDef_AutomorphicForm_BoundedGenuineCuspRealization317 lines · statements of 62 theoremsDef_AutomorphicForm_TwistedGeometricRemainder171 lines · statements of 57 theoremsDef_AutomorphicForm_TransversalMeasure129 lines · statements of 54 theoremsDef_AutomorphicForm_BorelSubgroup217 lines · statements of 43 theoremsDef_AutomorphicForm_TwistedCuspKernel56 lines · statements of 39 theoremsDef_AutomorphicForm_LocalWeightedOrbital208 lines · statements of 38 theoremsDef_AutomorphicForm_CentreCutSiegelSet562 lines · statements of 37 theoremsDef_AutomorphicForm_RationalTorusUnipotentQuotient46 lines · statements of 37 theoremsDef_AutomorphicForm_ArchSpherical67 lines · statements of 36 theoremsDef_AutomorphicForm_FnTwist105 lines · statements of 34 theoremsDef_AutomorphicForm_AdelicTracePushforward59 lines · statements of 33 theoremsDef_AutomorphicForm_ArithCuspRealization122 lines · statements of 33 theoremsDef_AutomorphicForm_ViaCompactCuspNotion75 lines · statements of 32 theoremsDef_AutomorphicForm_CuspidalSpectrumSubrep104 lines · statements of 30 theoremsDef_AutomorphicForm_Gamma0FundamentalSet124 lines · statements of 30 theoremsDef_AutomorphicForm_UnitFactorizableOfType78 lines · statements of 29 theoremsDef_AutomorphicForm_WindowedSiegelSet308 lines · statements of 28 theoremsDef_AutomorphicForm_GL2RealOrbitalTransforms62 lines · statements of 27 theoremsDef_AutomorphicForm_SiegelCovering355 lines · statements of 27 theoremsDef_AutomorphicForm_SigmaCentralizer62 lines · statements of 23 theoremsDef_AutomorphicForm_ProductionPins80 lines · statements of 22 theoremsDef_AutomorphicForm_TwistedCommutant204 lines · statements of 21 theoremsDef_AutomorphicForm_PeterssonIntegral23 lines · statements of 20 theoremsDef_AutomorphicForm_HeckeEigensystem113 lines · statements of 19 theoremsDef_AutomorphicForm_DihedralWeightOneLift31 lines · statements of 17 theoremsDef_AutomorphicForm_SmoothCuspRealization242 lines · statements of 17 theoremsDef_AutomorphicForm_SplitFibreIntegral329 lines · statements of 16 theoremsDef_AutomorphicForm_CentreCutSiegelSetAmple98 lines · statements of 15 theoremsDef_AutomorphicForm_RankinSelbergQuotientIntegral47 lines · statements of 14 theoremsDef_AutomorphicForm_ArchLoweringAnnihilated126 lines · statements of 12 theoremsDef_AutomorphicForm_RationalCentreUnipotentQuotient40 lines · statements of 12 theoremsDef_AutomorphicForm_GL2TwistedOrbitalTransforms104 lines · statements of 11 theoremsDef_AutomorphicForm_ArchLowestWeight100 lines · statements of 9 theoremsDef_AutomorphicForm_ComplexIwasawa26 lines · statements of 8 theoremsDef_AutomorphicForm_ProductionPinsCompact93 lines · statements of 7 theoremsDef_AutomorphicForm_ArchType190 lines · statements of 6 theoremsDef_AutomorphicForm_WeylSelectors173 lines · statements of 6 theoremsDef_AutomorphicForm_GL2RealKTypeModule97 lines · statements of 5 theoremsDef_AutomorphicForm_GaussTwist458 lines · statements of 5 theoremsDef_AutomorphicForm_ViaGeneralCuspNotion71 lines · statements of 5 theoremsDef_AutomorphicForm_WhittakerModelMultiplicityOne52 lines · statements of 3 theoremsDef_AutomorphicForm_CyclicBaseChangeLifting45 lines · statements of 2 theoremsDef_AutomorphicForm_GL2TwistedMonomialFibres55 lines · statements of 2 theoremsDef_AutomorphicForm_IwasawaShellIndex183 lines · statements of 2 theoremsDef_AutomorphicForm_HeckeEigensystemMap49 lines · statements of 1 theoremsDef_AutomorphicForm_SigmaConjugacy47 lines · statements of 1 theoremsDef_AutomorphicForm_ArchDerivCasimirComplexAPI382 lines · statements of 0 theoremsDef_AutomorphicForm_EisensteinScattering279 lines · statements of 0 theoremsDef_AutomorphicForm_FundamentalDomainExactVolume237 lines · statements of 0 theoremsDef_AutomorphicForm_FundamentalDomainVolume179 lines · statements of 0 theoremsDef_AutomorphicForm_Gamma0ExactVolume177 lines · statements of 0 theoremsDef_AutomorphicForm_HyperbolicMeasure130 lines · statements of 0 theoremsDef_AutomorphicForm_L2AutomorphicCarrier148 lines · statements of 0 theoremsDef_AutomorphicForm_L2ProductionInstance112 lines · statements of 0 theoremsDef_AutomorphicForm_LocalLFactor161 lines · statements of 0 theoremsDef_AutomorphicForm_ModularFundamentalDomain218 lines · statements of 0 theoremsDef_AutomorphicForm_ProductionNotionGateEigensystems43 lines · statements of 0 theoremsDef_AutomorphicForm_SiegelReduction173 lines · statements of 0 theoremsDef_AutomorphicForm_SiegelSetCover114 lines · statements of 0 theoremsDef_AutomorphicForm_TruncatedDomainPartition489 lines · statements of 0 theoremsDef_AutomorphicForm_WindowedSiegelTopology132 lines · statements of 0 theorems
LanglandsTunnell 84 modules
Def_LanglandsTunnell_ConverseData192 lines · statements of 581 theoremsDef_LanglandsTunnell_RSCarrier56 lines · statements of 405 theoremsDef_LanglandsTunnell_StandardLocalConstantsAt145 lines · statements of 373 theoremsDef_LanglandsTunnell_CubicInduction_MirabolicMajorant79 lines · statements of 361 theoremsDef_LanglandsTunnell_CubicLambda75 lines · statements of 308 theoremsDef_LanglandsTunnell_CubicInduction_Structure326 lines · statements of 307 theoremsDef_LanglandsTunnell_CubicInduction_ArchZeta3156 lines · statements of 299 theoremsDef_LanglandsTunnell_CubicInduction_LocalZeta3153 lines · statements of 284 theoremsDef_LanglandsTunnell_RankinSelbergEuler97 lines · statements of 280 theoremsDef_LanglandsTunnell_CubicInduction_GlobalZeta31159 lines · statements of 251 theoremsDef_LanglandsTunnell_CubicInduction_ArchCentre330 lines · statements of 210 theoremsDef_LanglandsTunnell_CubicInduction_TorusValues80 lines · statements of 208 theoremsDef_LanglandsTunnell_ArchBaseChange204 lines · statements of 206 theoremsDef_LanglandsTunnell_CubicInduction_AutomorphyDatum31244 lines · statements of 185 theoremsDef_LanglandsTunnell_RSCarrierSplit36 lines · statements of 177 theoremsDef_LanglandsTunnell_CubicInduction_JacquetVector350 lines · statements of 169 theoremsDef_LanglandsTunnell_CubicInduction_PrincipalSeries2426 lines · statements of 165 theoremsDef_LanglandsTunnell_LambdaSquared113 lines · statements of 160 theoremsDef_LanglandsTunnell_HeckeTate52 lines · statements of 147 theoremsDef_LanglandsTunnell_CubicInduction_CellBumps60 lines · statements of 145 theoremsDef_LanglandsTunnell_CubicInduction_Congruence48 lines · statements of 139 theoremsDef_LanglandsTunnell_ArchCasimirCompanion62 lines · statements of 124 theoremsDef_LanglandsTunnell_CubicInduction_PrincipalSeries3576 lines · statements of 102 theoremsDef_LanglandsTunnell_JLConverse302 lines · statements of 88 theoremsDef_LanglandsTunnell_CubicInduction_JacquetWhittaker209 lines · statements of 87 theoremsDef_LanglandsTunnell_DeltaLift47 lines · statements of 86 theoremsDef_LanglandsTunnell_TateLocalZeta144 lines · statements of 85 theoremsDef_LanglandsTunnell_CubicInduction_GodementSection160 lines · statements of 78 theoremsDef_LanglandsTunnell_ArtinCoreCTM510 lines · statements of 72 theoremsDef_LanglandsTunnell_TateLocalConstantsAt156 lines · statements of 63 theoremsDef_LanglandsTunnell_CubicInduction_SlabL2Cusp107 lines · statements of 53 theoremsDef_LanglandsTunnell_HonestLDatum95 lines · statements of 52 theoremsDef_LanglandsTunnell_RSGlobalIntegral43 lines · statements of 52 theoremsDef_LanglandsTunnell_RS22GlobalIntegral191 lines · statements of 50 theoremsDef_LanglandsTunnell_CubicInduction_DataOn121 lines · statements of 44 theoremsDef_LanglandsTunnell_ArchParam140 lines · statements of 31 theoremsDef_LanglandsTunnell_QuatH98 lines · statements of 24 theoremsDef_LanglandsTunnell_CubicInduction_HeckeDatum118 lines · statements of 19 theoremsDef_LanglandsTunnell_CubicInduction_IotaTorus88 lines · statements of 16 theoremsDef_LanglandsTunnell_CubicInduction_WhittakerBlock125 lines · statements of 16 theoremsDef_LanglandsTunnell_LiftTraceSeed103 lines · statements of 14 theoremsDef_LanglandsTunnell_ArchBessel21 lines · statements of 12 theoremsDef_LanglandsTunnell_ArtinFrobenius116 lines · statements of 10 theoremsDef_LanglandsTunnell_Converse_ExplicitWhittakerFunctions50 lines · statements of 10 theoremsDef_LanglandsTunnell_CubicInduction_AdelicEpstein59 lines · statements of 10 theoremsDef_LanglandsTunnell_CubicInduction_ArchSmooth328 lines · statements of 10 theoremsDef_LanglandsTunnell_CubicInduction_Carrier244 lines · statements of 10 theoremsDef_LanglandsTunnell_ExplicitLift26 lines · statements of 10 theoremsDef_LanglandsTunnell_ArchPlace121 lines · statements of 9 theoremsDef_LanglandsTunnell_DetDictionaryRow21 lines · statements of 8 theoremsDef_LanglandsTunnell_CubicInduction_Growth75 lines · statements of 7 theoremsDef_LanglandsTunnell_P52Interface30 lines · statements of 7 theoremsDef_LanglandsTunnell_RealizationDictionary43 lines · statements of 7 theoremsDef_LanglandsTunnell_CubicInduction_LocalWhittakerDatum25 lines · statements of 6 theoremsDef_LanglandsTunnell_CubicInduction_SpectralOperators334 lines · statements of 6 theoremsDef_LanglandsTunnell_JLData130 lines · statements of 6 theoremsDef_LanglandsTunnell_WeightOneRealizationCarriers81 lines · statements of 6 theoremsDef_LanglandsTunnell_C4Character177 lines · statements of 4 theoremsDef_LanglandsTunnell_C8Character203 lines · statements of 4 theoremsDef_LanglandsTunnell_CubicInduction_SlabL287 lines · statements of 4 theoremsDef_LanglandsTunnell_JLSynthesis277 lines · statements of 4 theoremsDef_LanglandsTunnell_ArchEpsilon80 lines · statements of 3 theoremsDef_LanglandsTunnell_CubicInduction_KFinite326 lines · statements of 3 theoremsDef_LanglandsTunnell_CubicInduction_SlabL2KernelCasimir43 lines · statements of 3 theoremsDef_LanglandsTunnell_BcWeight20 lines · statements of 2 theoremsDef_LanglandsTunnell_C8Tower151 lines · statements of 2 theoremsDef_LanglandsTunnell_CubicInduction_FnTwist3148 lines · statements of 2 theoremsDef_LanglandsTunnell_AnalyticGates41 lines · statements of 1 theoremsDef_LanglandsTunnell_CubicInduction_EnvelopingAction3218 lines · statements of 1 theoremsDef_LanglandsTunnell_GalRep32 lines · statements of 1 theoremsDef_LanglandsTunnell_TorusTransform394 lines · statements of 1 theoremsDef_LanglandsTunnell_CubicInduction_AdditiveJacquet1,011 lines · statements of 0 theoremsDef_LanglandsTunnell_CubicInduction_ArchSmoothSpace3185 lines · statements of 0 theoremsDef_LanglandsTunnell_CubicInduction_HeckeRepresentatives1,911 lines · statements of 0 theoremsDef_LanglandsTunnell_CubicInduction_SphericalValues400 lines · statements of 0 theoremsDef_LanglandsTunnell_IsAttached45 lines · statements of 0 theoremsDef_LanglandsTunnell_IsGaloisAttachmentOf25 lines · statements of 0 theoremsDef_LanglandsTunnell_Lift48437 lines · statements of 0 theoremsDef_LanglandsTunnell_NormClass292 lines · statements of 0 theoremsDef_LanglandsTunnell_OctahedralDatum67 lines · statements of 0 theoremsDef_LanglandsTunnell_SchwartzBruhatSpace68 lines · statements of 0 theoremsDef_LanglandsTunnell_SylowH39 lines · statements of 0 theoremsDef_LanglandsTunnell_TowerCounting49 lines · statements of 0 theoremsDef_LanglandsTunnell_TunnellExistenceCarriers41 lines · statements of 0 theorems
CerednikDrinfeld 83 modules
Def_CerednikDrinfeld_SpecialFormalModule658 lines · statements of 528 theoremsDef_CerednikDrinfeld_QMFineModuli123 lines · statements of 464 theoremsDef_CerednikDrinfeld_ClassSetGraph113 lines · statements of 393 theoremsDef_CerednikDrinfeld_QMModuli257 lines · statements of 330 theoremsDef_CerednikDrinfeld_CosetGraphAtPrime86 lines · statements of 312 theoremsDef_CerednikDrinfeld_GradedCartierModuleData125 lines · statements of 272 theoremsDef_CerednikDrinfeld_GradedCartierNModule206 lines · statements of 264 theoremsDef_CerednikDrinfeld_ShimuraCurve357 lines · statements of 264 theoremsDef_CerednikDrinfeld_QMCoarseModuli95 lines · statements of 250 theoremsDef_CerednikDrinfeld_QMRigidification180 lines · statements of 239 theoremsDef_CerednikDrinfeld_SchemeNilpPoints57 lines · statements of 236 theoremsDef_CerednikDrinfeld_DrinfeldQuadruple179 lines · statements of 232 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlaneFunctor480 lines · statements of 232 theoremsDef_CerednikDrinfeld_QMFormalModuleOf58 lines · statements of 231 theoremsDef_CerednikDrinfeld_CartierModuleModel266 lines · statements of 228 theoremsDef_CerednikDrinfeld_HeckeTower84 lines · statements of 225 theoremsDef_CerednikDrinfeld_DrinfeldHolomorphic783 lines · statements of 224 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlaneDatum114 lines · statements of 221 theoremsDef_CerednikDrinfeld_SpecialFormalFunctorG153 lines · statements of 211 theoremsDef_CerednikDrinfeld_CartierQuadruple316 lines · statements of 199 theoremsDef_CerednikDrinfeld_QMModuliProps146 lines · statements of 197 theoremsDef_CerednikDrinfeld_QMFineModuliT80 lines · statements of 145 theoremsDef_CerednikDrinfeld_QMCanonicalPol43 lines · statements of 140 theoremsDef_CerednikDrinfeld_BruhatTitsTree109 lines · statements of 136 theoremsDef_CerednikDrinfeld_AlgFunctorConst19 lines · statements of 130 theoremsDef_CerednikDrinfeld_MumfordQuotient377 lines · statements of 108 theoremsDef_CerednikDrinfeld_SchottkyTreeAction168 lines · statements of 107 theoremsDef_CerednikDrinfeld_CartierGradedPiece65 lines · statements of 105 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlanePoints204 lines · statements of 95 theoremsDef_CerednikDrinfeld_CartierStructureConstants350 lines · statements of 93 theoremsDef_CerednikDrinfeld_QMRigidificationLevel35 lines · statements of 91 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlaneChartRings255 lines · statements of 85 theoremsDef_CerednikDrinfeld_QMIsogeny36 lines · statements of 76 theoremsDef_CerednikDrinfeld_QMModuliTower94 lines · statements of 76 theoremsDef_CerednikDrinfeld_DescentIntertwining_v283 lines · statements of 73 theoremsDef_CerednikDrinfeld_MumfordVertexType33 lines · statements of 65 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlaneFrame50 lines · statements of 64 theoremsDef_CerednikDrinfeld_QMModuliTowerD93 lines · statements of 62 theoremsDef_CerednikDrinfeld_DrinfeldQuadrupleRelations146 lines · statements of 55 theoremsDef_CerednikDrinfeld_DescentIntertwiningBase70 lines · statements of 54 theoremsDef_CerednikDrinfeld_MumfordPeriod120 lines · statements of 54 theoremsDef_CerednikDrinfeld_ThetaMer42 lines · statements of 47 theoremsDef_CerednikDrinfeld_QMStructureOnPolarised98 lines · statements of 46 theoremsDef_CerednikDrinfeld_FakeEllipticFrobenius91 lines · statements of 45 theoremsDef_CerednikDrinfeld_EdgeFamilyConstants99 lines · statements of 42 theoremsDef_CerednikDrinfeld_PeriodMapSpec42 lines · statements of 40 theoremsDef_CerednikDrinfeld_DiscreteProjectiveAction20 lines · statements of 39 theoremsDef_CerednikDrinfeld_MumfordTower102 lines · statements of 33 theoremsDef_CerednikDrinfeld_ModuliPackageDeformation75 lines · statements of 32 theoremsDef_CerednikDrinfeld_CartierQuadrupleVia94 lines · statements of 30 theoremsDef_CerednikDrinfeld_PeriodMap66 lines · statements of 26 theoremsDef_CerednikDrinfeld_DrinfeldUpperHalfPlane184 lines · statements of 25 theoremsDef_CerednikDrinfeld_FormalQuotientDatum177 lines · statements of 24 theoremsDef_CerednikDrinfeld_EquivariantUniformization58 lines · statements of 19 theoremsDef_CerednikDrinfeld_MumfordQuotientNormalizer114 lines · statements of 16 theoremsDef_CerednikDrinfeld_QMLatticeAction91 lines · statements of 15 theoremsDef_CerednikDrinfeld_FormalUpperHalfPlaneCharts176 lines · statements of 14 theoremsDef_CerednikDrinfeld_OmegaOrdAt59 lines · statements of 13 theoremsDef_CerednikDrinfeld_CriticalIndexChart388 lines · statements of 12 theoremsDef_CerednikDrinfeld_ModuliPackageDescent86 lines · statements of 12 theoremsDef_CerednikDrinfeld_MumfordNrPresentation84 lines · statements of 12 theoremsDef_CerednikDrinfeld_Ribbon135 lines · statements of 12 theoremsDef_CerednikDrinfeld_MumfordGlue128 lines · statements of 11 theoremsDef_CerednikDrinfeld_MumfordGlueCore127 lines · statements of 11 theoremsDef_CerednikDrinfeld_QMModuliPropsD43 lines · statements of 11 theoremsDef_CerednikDrinfeld_RigidifiedPairClassModel204 lines · statements of 11 theoremsDef_CerednikDrinfeld_QMFormalCompletionAlong23 lines · statements of 10 theoremsDef_CerednikDrinfeld_TwoPlaceTorsionDatum151 lines · statements of 9 theoremsDef_CerednikDrinfeld_MumfordGlueLevel113 lines · statements of 8 theoremsDef_CerednikDrinfeld_MumfordUniformization99 lines · statements of 6 theoremsDef_CerednikDrinfeld_ToricUniformization76 lines · statements of 6 theoremsDef_CerednikDrinfeld_QMIsogenyPairRep72 lines · statements of 5 theoremsDef_CerednikDrinfeld_OmegaTubes93 lines · statements of 4 theoremsDef_CerednikDrinfeld_ODModuleFrobeniusTwist238 lines · statements of 3 theoremsDef_CerednikDrinfeld_WalkOverlap107 lines · statements of 3 theoremsDef_CerednikDrinfeld_CritChartEndMatrix223 lines · statements of 2 theoremsDef_CerednikDrinfeld_JPrimeTorsionDatum57 lines · statements of 2 theoremsDef_CerednikDrinfeld_OmegaModuliPackage93 lines · statements of 2 theoremsDef_CerednikDrinfeld_CartierLMapFibre96 lines · statements of 1 theoremsDef_CerednikDrinfeld_CartierNModule249 lines · statements of 1 theoremsDef_CerednikDrinfeld_LubinTateModule1,125 lines · statements of 1 theoremsDef_CerednikDrinfeld_QMModuliWitnessD80 lines · statements of 1 theoremsDef_CerednikDrinfeld_StandardFormalODModule1,105 lines · statements of 1 theorems
AlgebraicCurve 72 modules
Def_AlgebraicCurve_TwoChartIntegralModel380 lines · statements of 1,223 theoremsDef_AlgebraicCurve_IsCurveOver77 lines · statements of 1,013 theoremsDef_AlgebraicCurve_ConstantReduction128 lines · statements of 943 theoremsDef_AlgebraicCurve_RegularProlongation85 lines · statements of 733 theoremsDef_AlgebraicCurve_DivisorClassGroup485 lines · statements of 660 theoremsDef_AlgebraicCurve_CurveModel86 lines · statements of 644 theoremsDef_AlgebraicCurve_ResidueDiscs271 lines · statements of 553 theoremsDef_AlgebraicCurve_Repartitions150 lines · statements of 545 theoremsDef_AlgebraicCurve_SemistableCharts189 lines · statements of 375 theoremsDef_AlgebraicCurve_Correspondence347 lines · statements of 352 theoremsDef_AlgebraicCurve_BaseChangeGalois356 lines · statements of 322 theoremsDef_AlgebraicCurve_AdelicIndex436 lines · statements of 278 theoremsDef_AlgebraicCurve_PlaceEvaluation87 lines · statements of 275 theoremsDef_AlgebraicCurve_SemistableModel217 lines · statements of 256 theoremsDef_AlgebraicCurve_GluedPic0277 lines · statements of 251 theoremsDef_AlgebraicCurve_RatFuncPlaces398 lines · statements of 170 theoremsDef_AlgebraicCurve_DivisorPushPull736 lines · statements of 130 theoremsDef_AlgebraicCurve_RegularDifferentials47 lines · statements of 129 theoremsDef_AlgebraicCurve_RelCartier103 lines · statements of 111 theoremsDef_AlgebraicCurve_CanonicalDivisor43 lines · statements of 110 theoremsDef_AlgebraicCurve_GluedPic0Functoriality217 lines · statements of 103 theoremsDef_AlgebraicCurve_RatFuncPlaceInfty45 lines · statements of 90 theoremsDef_AlgebraicCurve_WeilDatum82 lines · statements of 71 theoremsDef_AlgebraicCurve_Differentials86 lines · statements of 64 theoremsDef_AlgebraicCurve_CechSectionsOfDivisor267 lines · statements of 57 theoremsDef_AlgebraicCurve_ChordalProximity26 lines · statements of 55 theoremsDef_AlgebraicCurve_CurveModelConstruction2,086 lines · statements of 52 theoremsDef_AlgebraicCurve_LocalResidue309 lines · statements of 45 theoremsDef_AlgebraicCurve_TotallyDegenerateCovering_Hom318 lines · statements of 45 theoremsDef_AlgebraicCurve_DifferentialPushPull80 lines · statements of 44 theoremsDef_AlgebraicCurve_WeilOfKaehler134 lines · statements of 38 theoremsDef_AlgebraicCurve_PlacesOf61 lines · statements of 33 theoremsDef_AlgebraicCurve_Pic0Congr123 lines · statements of 30 theoremsDef_AlgebraicCurve_PlacesOverDVR507 lines · statements of 30 theoremsDef_AlgebraicCurve_FunctionFieldWeilPairingDivisorial791 lines · statements of 29 theoremsDef_AlgebraicCurve_ComplexLineIntegral102 lines · statements of 27 theoremsDef_AlgebraicCurve_PlaceTaylorCoeff94 lines · statements of 26 theoremsDef_AlgebraicCurve_RiemannRochRows67 lines · statements of 24 theoremsDef_AlgebraicCurve_CellDissection156 lines · statements of 22 theoremsDef_AlgebraicCurve_CanonicalLocalResidueInstanceV22,174 lines · statements of 21 theoremsDef_AlgebraicCurve_CechH1PushPull158 lines · statements of 18 theoremsDef_AlgebraicCurve_GluedPic0SliceOps99 lines · statements of 18 theoremsDef_AlgebraicCurve_PlaceEvaluationAlgebra161 lines · statements of 17 theoremsDef_AlgebraicCurve_PoleDivisorPackage102 lines · statements of 17 theoremsDef_AlgebraicCurve_CycleChowForm141 lines · statements of 16 theoremsDef_AlgebraicCurve_PolarDifferentials201 lines · statements of 16 theoremsDef_AlgebraicCurve_ConstantFieldPullback273 lines · statements of 13 theoremsDef_AlgebraicCurve_StandardAnnulus1,656 lines · statements of 12 theoremsDef_AlgebraicCurve_TateResidueCurrency450 lines · statements of 12 theoremsDef_AlgebraicCurve_SerrePairing260 lines · statements of 11 theoremsDef_AlgebraicCurve_FibreResidueIdentityAlong27 lines · statements of 10 theoremsDef_AlgebraicCurve_KaehlerToFunctionField133 lines · statements of 10 theoremsDef_AlgebraicCurve_PlaceCompletion530 lines · statements of 8 theoremsDef_AlgebraicCurve_SemistableChartsComap359 lines · statements of 7 theoremsDef_AlgebraicCurve_FrobeniusEndo50 lines · statements of 5 theoremsDef_AlgebraicCurve_PlaceDepth162 lines · statements of 5 theoremsDef_AlgebraicCurve_RatFuncPlaceClassification125 lines · statements of 5 theoremsDef_AlgebraicCurve_TotallyDegenerateCovering93 lines · statements of 5 theoremsDef_AlgebraicCurve_TwoChartIntegralModelCharts353 lines · statements of 5 theoremsDef_AlgebraicCurve_AffinoidCentre39 lines · statements of 4 theoremsDef_AlgebraicCurve_LogDeRhamH1421 lines · statements of 3 theoremsDef_AlgebraicCurve_NodalPic095 lines · statements of 3 theoremsDef_AlgebraicCurve_CanonicalLocalResidueInstance695 lines · statements of 2 theoremsDef_AlgebraicCurve_FrobeniusEndoPic0323 lines · statements of 2 theoremsDef_AlgebraicCurve_GluedPic0Pushforward144 lines · statements of 2 theoremsDef_AlgebraicCurve_JacobianH1Autoduality338 lines · statements of 2 theoremsDef_AlgebraicCurve_Pic0BaseChange126 lines · statements of 2 theoremsDef_AlgebraicCurve_GluedPic0CrossFunctionality220 lines · statements of 1 theoremsDef_AlgebraicCurve_CurveModelSmooth297 lines · statements of 0 theoremsDef_AlgebraicCurve_CurveModelTransport226 lines · statements of 0 theoremsDef_AlgebraicCurve_SymmetricPower129 lines · statements of 0 theoremsDef_AlgebraicCurve_UniversalDivisor168 lines · statements of 0 theorems
WeierstrassCurve 61 modules
Def_WeierstrassCurve_DrinfeldBasisGlobal118 lines · statements of 473 theoremsDef_WeierstrassCurve_DrinfeldLevelFunctor109 lines · statements of 419 theoremsDef_WeierstrassCurve_SectionAtOrigin52 lines · statements of 371 theoremsDef_WeierstrassCurve_ProjModel346 lines · statements of 300 theoremsDef_WeierstrassCurve_DrinfeldTransportPin60 lines · statements of 299 theoremsDef_WeierstrassCurve_FormalGroupLaw973 lines · statements of 207 theoremsDef_WeierstrassCurve_RationalEnd83 lines · statements of 157 theoremsDef_WeierstrassCurve_PointChart47 lines · statements of 148 theoremsDef_WeierstrassCurve_ProjModel_GroupLawVocabulary2,273 lines · statements of 135 theoremsDef_WeierstrassCurve_VariableChangePointEquiv161 lines · statements of 90 theoremsDef_WeierstrassCurve_FormalGroup1,583 lines · statements of 88 theoremsDef_WeierstrassCurve_ReductionMap254 lines · statements of 84 theoremsDef_WeierstrassCurve_OddOrderSummingSet35 lines · statements of 69 theoremsDef_WeierstrassCurve_Velu99 lines · statements of 67 theoremsDef_WeierstrassCurve_KernelIdeal26 lines · statements of 49 theoremsDef_WeierstrassCurve_GenusOnePlaceGateCentred41 lines · statements of 44 theoremsDef_WeierstrassCurve_HasseInvariant25 lines · statements of 41 theoremsDef_WeierstrassCurve_FullKernelQuotient143 lines · statements of 31 theoremsDef_WeierstrassCurve_ReduceHom490 lines · statements of 30 theoremsDef_WeierstrassCurve_CyclicQuotientJ208 lines · statements of 29 theoremsDef_WeierstrassCurve_DrinfeldBasisRelative48 lines · statements of 23 theoremsDef_WeierstrassCurve_VeluPointMap87 lines · statements of 23 theoremsDef_WeierstrassCurve_VeluQuotientMap75 lines · statements of 21 theoremsDef_WeierstrassCurve_VeluOrderTwo50 lines · statements of 18 theoremsDef_WeierstrassCurve_DrinfeldLevelFunctorRestrict138 lines · statements of 17 theoremsDef_WeierstrassCurve_VeluPointMap2118 lines · statements of 13 theoremsDef_WeierstrassCurve_RatPointHom58 lines · statements of 10 theoremsDef_WeierstrassCurve_PeuRamifiee23 lines · statements of 9 theoremsDef_WeierstrassCurve_VariableChangeSeries30 lines · statements of 9 theoremsDef_WeierstrassCurve_KernelPolynomial71 lines · statements of 7 theoremsDef_WeierstrassCurve_ProjModel_AddFormulas654 lines · statements of 6 theoremsDef_WeierstrassCurve_KohelQuotient135 lines · statements of 5 theoremsDef_WeierstrassCurve_FunctionFieldQuadratic151 lines · statements of 4 theoremsDef_WeierstrassCurve_LevelThreeModulus425 lines · statements of 4 theoremsDef_WeierstrassCurve_ConductorLevel31 lines · statements of 3 theoremsDef_WeierstrassCurve_GenusOnePic0172 lines · statements of 3 theoremsDef_WeierstrassCurve_ProjModel_ThirdLawCharts456 lines · statements of 3 theoremsDef_WeierstrassCurve_DivPolyMulFormula1,751 lines · statements of 2 theoremsDef_WeierstrassCurve_Generic145 lines · statements of 2 theoremsDef_WeierstrassCurve_MapPoint115 lines · statements of 2 theoremsDef_WeierstrassCurve_Mlc1RowStatement22 lines · statements of 2 theoremsDef_WeierstrassCurve_ModularityLiftingConductor43 lines · statements of 2 theoremsDef_WeierstrassCurve_ModularityProps55 lines · statements of 2 theoremsDef_WeierstrassCurve_VeluQuotientOfSums32 lines · statements of 2 theoremsDef_WeierstrassCurve_LegendreModulus77 lines · statements of 1 theoremsDef_WeierstrassCurve_PointAddEquivOfEq22 lines · statements of 1 theoremsDef_WeierstrassCurve_VeluVariableChange113 lines · statements of 1 theoremsDef_WeierstrassCurve_AddFormula115 lines · statements of 0 theoremsDef_WeierstrassCurve_DivPolyMulFormulaCore327 lines · statements of 0 theoremsDef_WeierstrassCurve_EDSEngine1,870 lines · statements of 0 theoremsDef_WeierstrassCurve_FrobeniusCardHom262 lines · statements of 0 theoremsDef_WeierstrassCurve_ProjModel_ThirdAddFormulas309 lines · statements of 0 theoremsDef_WeierstrassCurve_RatPointMap_probe21 lines · statements of 0 theoremsDef_WeierstrassCurve_Semistability20 lines · statements of 0 theoremsDef_WeierstrassCurve_ThreeFiveSwitchConditioned17 lines · statements of 0 theoremsDef_WeierstrassCurve_TorsionIntegral1,234 lines · statements of 0 theoremsDef_WeierstrassCurve_VeluBundledMap96 lines · statements of 0 theoremsDef_WeierstrassCurve_VeluEquivariance201 lines · statements of 0 theoremsDef_WeierstrassCurve_VeluOrderTwoShortNF68 lines · statements of 0 theoremsDef_WeierstrassCurve_VeluQuotientJInvariant93 lines · statements of 0 theoremsDef_WeierstrassCurve_ZeroComponentReduction1,104 lines · statements of 0 theorems
GroupCohomology 49 modules
Def_GroupCohomology_ContinuousUnramified251 lines · statements of 205 theoremsDef_GroupCohomology_ContinuousUnramifiedLevel218 lines · statements of 127 theoremsDef_GroupCohomology_TateCohomology155 lines · statements of 125 theoremsDef_GroupCohomology_ContinuousH2135 lines · statements of 98 theoremsDef_GroupCohomology_ContinuousUnramifiedLevelMap165 lines · statements of 71 theoremsDef_GroupCohomology_ContinuousH191 lines · statements of 65 theoremsDef_GroupCohomology_LevelSubgroup29 lines · statements of 53 theoremsDef_GroupCohomology_TangentSpace189 lines · statements of 51 theoremsDef_GroupCohomology_ContinuousH2Map104 lines · statements of 44 theoremsDef_GroupCohomology_TateSeam178 lines · statements of 44 theoremsDef_GroupCohomology_TateDimensionShift76 lines · statements of 40 theoremsDef_GroupCohomology_GaloisUnitsInflation51 lines · statements of 38 theoremsDef_GroupCohomology_TateShiftMaps49 lines · statements of 37 theoremsDef_GroupCohomology_ContinuousDuality35 lines · statements of 35 theoremsDef_GroupCohomology_Kummer210 lines · statements of 31 theoremsDef_GroupCohomology_ContinuousUnramifiedLevelInflation80 lines · statements of 30 theoremsDef_GroupCohomology_RelationModule92 lines · statements of 30 theoremsDef_GroupCohomology_CochainCup31 lines · statements of 29 theoremsDef_GroupCohomology_CyclicCarry26 lines · statements of 29 theoremsDef_GroupCohomology_ContinuousH2Inflation149 lines · statements of 28 theoremsDef_GroupCohomology_IsGradedCupProduct26 lines · statements of 28 theoremsDef_GroupCohomology_Selmer155 lines · statements of 24 theoremsDef_GroupCohomology_CupProduct232 lines · statements of 23 theoremsDef_GroupCohomology_IsTateCupProduct48 lines · statements of 23 theoremsDef_GroupCohomology_LocalInvariant39 lines · statements of 23 theoremsDef_GroupCohomology_LocalBridge40 lines · statements of 18 theoremsDef_GroupCohomology_LocallyConstantClasses51 lines · statements of 15 theoremsDef_GroupCohomology_RepPi50 lines · statements of 10 theoremsDef_GroupCohomology_DClassCoeff127 lines · statements of 9 theoremsDef_GroupCohomology_RelationModuleRes67 lines · statements of 9 theoremsDef_GroupCohomology_Corestriction2198 lines · statements of 7 theoremsDef_GroupCohomology_GaloisSUnits90 lines · statements of 7 theoremsDef_GroupCohomology_RelationHomDefect84 lines · statements of 7 theoremsDef_GroupCohomology_TateDimensionShiftMaps86 lines · statements of 7 theoremsDef_GroupCohomology_TateTwist74 lines · statements of 7 theoremsDef_GroupCohomology_GlobalBridge33 lines · statements of 6 theoremsDef_GroupCohomology_SplittingModule159 lines · statements of 6 theoremsDef_GroupCohomology_TransferHecke211 lines · statements of 6 theoremsDef_GroupCohomology_RepCokernel37 lines · statements of 5 theoremsDef_GroupCohomology_CyclotomicQuotientH2Rep83 lines · statements of 4 theoremsDef_GroupCohomology_RepImage52 lines · statements of 4 theoremsDef_GroupCohomology_LevelConstantHom42 lines · statements of 3 theoremsDef_GroupCohomology_CorestrictionFin35 lines · statements of 2 theoremsDef_GroupCohomology_SelmerAdm87 lines · statements of 1 theoremsDef_GroupCohomology_TateResCor244 lines · statements of 1 theoremsDef_GroupCohomology_LevelQuotient66 lines · statements of 0 theoremsDef_GroupCohomology_PoitouTate58 lines · statements of 0 theoremsDef_GroupCohomology_RepToIntRep49 lines · statements of 0 theoremsDef_GroupCohomology_SelmerLe63 lines · statements of 0 theorems
NumberField 46 modules
Def_NumberField_TateGlobalZeta92 lines · statements of 1,077 theoremsDef_NumberField_AdelicHaar206 lines · statements of 642 theoremsDef_NumberField_PrincipalLevel30 lines · statements of 573 theoremsDef_NumberField_AdelicBox538 lines · statements of 557 theoremsDef_NumberField_AdelicHeight324 lines · statements of 525 theoremsDef_NumberField_StandardGlobalAddCharRat725 lines · statements of 377 theoremsDef_NumberField_AdelicLevel814 lines · statements of 360 theoremsDef_NumberField_IdeleProductMeasure695 lines · statements of 236 theoremsDef_NumberField_PlaceDecompositionAction272 lines · statements of 201 theoremsDef_NumberField_NormPowChar49 lines · statements of 135 theoremsDef_NumberField_LevelArithmeticModP314 lines · statements of 107 theoremsDef_NumberField_AdelicFourier116 lines · statements of 104 theoremsDef_NumberField_AdelicTraceFin205 lines · statements of 86 theoremsDef_NumberField_ArchimedeanIdeleModule165 lines · statements of 81 theoremsDef_NumberField_SUnitsMax69 lines · statements of 68 theoremsDef_NumberField_SIdeleModule115 lines · statements of 63 theoremsDef_NumberField_PlaceAbove33 lines · statements of 61 theoremsDef_NumberField_PlaceTransport210 lines · statements of 53 theoremsDef_NumberField_SelmerRepModP185 lines · statements of 41 theoremsDef_NumberField_IdeleLocalInvariant50 lines · statements of 27 theoremsDef_NumberField_SUnitsModule109 lines · statements of 19 theoremsDef_NumberField_IdeleBox172 lines · statements of 16 theoremsDef_NumberField_InfinitePlaceTransport66 lines · statements of 12 theoremsDef_NumberField_BrauerLocalInvariantChar53 lines · statements of 10 theoremsDef_NumberField_BrauerLocalInvariantPresentation49 lines · statements of 9 theoremsDef_NumberField_KummerCharacter49 lines · statements of 8 theoremsDef_NumberField_FiniteSIdeleModule55 lines · statements of 7 theoremsDef_NumberField_CompletedRayL35 lines · statements of 6 theoremsDef_NumberField_Completion_Finite66 lines · statements of 6 theorems · adapted from upstreamDef_NumberField_RayCharacterData86 lines · statements of 5 theoremsDef_NumberField_AdelicTraceProducer225 lines · statements of 4 theoremsDef_NumberField_SArchIdeleModule83 lines · statements of 3 theoremsDef_NumberField_IsSplitPrime18 lines · statements of 2 theoremsDef_NumberField_AdelicVolume213 lines · statements of 1 theoremsDef_NumberField_StandardGlobalAddChar117 lines · statements of 1 theoremsDef_NumberField_AdelicCentre108 lines · statements of 0 theoremsDef_NumberField_Completion_HenselianLocalRing169 lines · statements of 0 theoremsDef_NumberField_EuclideanIdealLattice35 lines · statements of 0 theoremsDef_NumberField_Extension199 lines · statements of 0 theorems · adapted from upstreamDef_NumberField_HeightOneSpectrum16 lines · statements of 0 theorems · adapted from upstreamDef_NumberField_InfiniteAdeleRing_BaseChangeData361 lines · statements of 0 theoremsDef_NumberField_IntegralAdelicTrace396 lines · statements of 0 theoremsDef_NumberField_NormResidueCharacter352 lines · statements of 0 theoremsDef_NumberField_PrimeNormSums296 lines · statements of 0 theoremsDef_NumberField_SIdeleClassModule145 lines · statements of 0 theoremsDef_NumberField_SiegelVolume457 lines · statements of 0 theorems
Mathlib 42 modules
Def_Mathlib_RingTheory_Valuation_UpperRamificationGroup375 lines · statements of 39 theoremsDef_Mathlib_Algebra_IsDirectLimit154 lines · statements of 24 theorems · adapted from upstreamDef_Mathlib_RingTheory_Invariant_FixedSubringLocal203 lines · statements of 20 theoremsDef_Mathlib_LinearAlgebra_Countable16 lines · statements of 13 theorems · adapted from upstreamDef_Mathlib_RightActionInstances179 lines · statements of 9 theorems · adapted from upstreamDef_Mathlib_RingTheory_Valuation_LowerRamificationGroupDepth267 lines · statements of 7 theoremsDef_Mathlib_RingTheory_Valuation_LowerRamificationGroup214 lines · statements of 4 theoremsDef_Mathlib_RingTheory_SmoothAlgebraOverFieldRegularStalks226 lines · statements of 1 theoremsDef_Mathlib_RingTheory_SmoothFieldFiberRegularStalksStandardSmoothReduction215 lines · statements of 1 theoremsDef_Mathlib_Algebra_Algebra_Hom141 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_CategoryTheory_Corepresentable62 lines · statements of 0 theoremsDef_Mathlib_FieldTheory_RatFuncImperfectionDegree390 lines · statements of 0 theoremsDef_Mathlib_IsModuleTopology511 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_MeasureTheory_Constructions_BorelSpace_RestrictedProduct13 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_MeasureTheory_Function_L2KernelOperator546 lines · statements of 0 theoremsDef_Mathlib_MeasureTheory_Group_Action106 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_MeasureTheory_Group_Measure18 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_MeasureTheory_Measure_Typeclasses_Finite19 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Order_Filter_Cofinite13 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_RingTheory_DedekindDomain_AdicValuation32 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_RingTheory_Ideal_Quotient_Basic11 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_RingTheory_Invariant_FixedSubringGaloisGroup21 lines · statements of 0 theoremsDef_Mathlib_RingTheory_KmfloorsFiberPolynomialRegularAscent270 lines · statements of 0 theoremsDef_Mathlib_RingTheory_KmfloorsGlueFiberLocalizationQuotientEngine511 lines · statements of 0 theoremsDef_Mathlib_RingTheory_LocalRing_Defs11 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_RingTheory_Localization_BaseChange79 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_RingTheory_RegularLocalRingFlatLocalAscent264 lines · statements of 0 theoremsDef_Mathlib_RingTheory_RegularLocalRingFlatLocalAscentV2416 lines · statements of 0 theoremsDef_Mathlib_RingTheory_RegularLocalRingQuotientRegular317 lines · statements of 0 theoremsDef_Mathlib_RingTheory_Valuation_LowerRamificationGroupGenerator273 lines · statements of 0 theoremsDef_Mathlib_RingTheory_Valuation_LowerRamificationGroupSubgroup175 lines · statements of 0 theoremsDef_Mathlib_RingTheory_Valuation_LowerRamificationGroupUniformizerClass315 lines · statements of 0 theoremsDef_Mathlib_RingTheory_Valuation_UpperRamificationGroupPsi420 lines · statements of 0 theoremsDef_Mathlib_Topology_Algebra_ContinuousMonoidHom51 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_Group_Units8 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_Module_Quotient38 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_RestrictedProduct_Basic286 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_RestrictedProduct_Equiv548 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_RestrictedProduct_TopologicalSpace577 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_UniformRing40 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Algebra_Valued_WithZeroMulInt92 lines · statements of 0 theorems · adapted from upstreamDef_Mathlib_Topology_Bases17 lines · statements of 0 theorems · adapted from upstream
CuspForm 32 modules
Def_CuspForm_HeckeLocal441 lines · statements of 165 theoremsDef_CuspForm_Newforms73 lines · statements of 157 theoremsDef_CuspForm_HeckeAlgebra94 lines · statements of 148 theoremsDef_CuspForm_PrimitiveFormGamma173 lines · statements of 128 theoremsDef_CuspForm_HeckeGaloisRepDatum39 lines · statements of 112 theoremsDef_CuspForm_IntegralStructure9 lines · statements of 104 theoremsDef_CuspForm_AdelicLift50 lines · statements of 93 theoremsDef_CuspForm_ModPForms29 lines · statements of 92 theoremsDef_CuspForm_AdelicLiftGamma150 lines · statements of 39 theoremsDef_CuspForm_HeckeOperatorFormsGammaH263 lines · statements of 36 theoremsDef_CuspForm_HeckeEvalForms50 lines · statements of 28 theoremsDef_CuspForm_TwoCuspLattice226 lines · statements of 21 theoremsDef_CuspForm_TWLevelHeckeRing267 lines · statements of 18 theoremsDef_CuspForm_IntegralLattice33 lines · statements of 17 theoremsDef_CuspForm_HeckeModuleCornerRealization58 lines · statements of 16 theoremsDef_CuspForm_AtkinLehnerOperator65 lines · statements of 14 theoremsDef_CuspForm_AuxLevelHeckeModuleBase61 lines · statements of 12 theoremsDef_CuspForm_CornerPairingFamily148 lines · statements of 11 theoremsDef_CuspForm_LevelLoweringTrace46 lines · statements of 11 theoremsDef_CuspForm_TWLevelHeckeModule183 lines · statements of 11 theoremsDef_CuspForm_Gamma1HeckeOperators681 lines · statements of 10 theoremsDef_CuspForm_AuxLevelHeckeModule65 lines · statements of 9 theoremsDef_CuspForm_LatticeHeckeFamily32 lines · statements of 7 theoremsDef_CuspForm_Petersson31 lines · statements of 6 theoremsDef_CuspForm_EigenformCoefficientRing43 lines · statements of 3 theoremsDef_CuspForm_NewLattice158 lines · statements of 3 theoremsDef_CuspForm_PeterssonOn32 lines · statements of 3 theoremsDef_CuspForm_AuxLevelHeckeModuleMid61 lines · statements of 2 theoremsDef_CuspForm_QCoeffLinear31 lines · statements of 2 theoremsDef_CuspForm_HeckeWord104 lines · statements of 1 theoremsDef_CuspForm_HeckeULower47 lines · statements of 0 theoremsDef_CuspForm_PeterssonCoset745 lines · statements of 0 theorems
GaloisRep 24 modules
Def_GaloisRep_Flat58 lines · statements of 500 theoremsDef_GaloisRep_TameCharacter13 lines · statements of 373 theoremsDef_GaloisRep_Residual106 lines · statements of 298 theoremsDef_GaloisRep_LocalConditions39 lines · statements of 213 theoremsDef_GaloisRep_CompletionBridge69 lines · statements of 134 theoremsDef_GaloisRep_Adic208 lines · statements of 97 theoremsDef_GaloisRep_ResidualEquiv55 lines · statements of 65 theoremsDef_GaloisRep_AdZero71 lines · statements of 56 theoremsDef_GaloisRep_DeformationRingData47 lines · statements of 55 theoremsDef_GaloisRep_RatLocalizedAtResidue38 lines · statements of 44 theoremsDef_GaloisRep_LocalFlatClasses65 lines · statements of 41 theoremsDef_GaloisRep_StrictOrdinary50 lines · statements of 35 theoremsDef_GaloisRep_ComplexConjugation63 lines · statements of 34 theoremsDef_GaloisRep_DeformationCondition75 lines · statements of 19 theoremsDef_GaloisRep_OrdinaryUnitClasses50 lines · statements of 11 theoremsDef_GaloisRep_ConditionLifts43 lines · statements of 10 theoremsDef_GaloisRep_FrobeniusPowerDense14 lines · statements of 10 theoremsDef_GaloisRep_ModThreeCyclotomic25 lines · statements of 9 theoremsDef_GaloisRep_GlobalUnramifiedAt19 lines · statements of 4 theoremsDef_GaloisRep_DeligneOrdinaryShape26 lines · statements of 3 theoremsDef_GaloisRep_AdZeroMatrixGlue31 lines · statements of 2 theoremsDef_GaloisRep_Twist141 lines · statements of 1 theoremsDef_GaloisRep_InertiaRing533 lines · statements of 0 theoremsDef_GaloisRep_WeilPairing41 lines · statements of 0 theorems
MvFormalGroup 19 modules
Def_MvFormalGroup_NegV2919 lines · statements of 537 theoremsDef_MvFormalGroup_CartierModule1,220 lines · statements of 173 theoremsDef_MvFormalGroup_CartierModuleHomothety235 lines · statements of 139 theoremsDef_MvFormalGroup_CartierModuleIntVerschiebung442 lines · statements of 130 theoremsDef_MvFormalGroup_CartierModuleWittAction677 lines · statements of 125 theoremsDef_MvFormalGroup_CartierModuleBaseChange361 lines · statements of 93 theoremsDef_MvFormalGroup_BasicV2427 lines · statements of 91 theoremsDef_MvFormalGroup_PointsV2485 lines · statements of 70 theoremsDef_MvFormalGroup_TwoCocycle111 lines · statements of 40 theoremsDef_MvFormalGroup_EndRingV21,036 lines · statements of 29 theoremsDef_MvFormalGroup_BigWittLaw132 lines · statements of 15 theoremsDef_MvFormalGroup_ArtinHasse194 lines · statements of 14 theoremsDef_MvFormalGroup_BigWittFrobenius496 lines · statements of 10 theoremsDef_MvFormalGroup_IsShiftBy26 lines · statements of 9 theoremsDef_MvFormalGroup_Deformation37 lines · statements of 6 theoremsDef_MvFormalGroup_WittPointFamily612 lines · statements of 4 theoremsDef_MvFormalGroup_FirstOrderDeformation34 lines · statements of 2 theoremsDef_MvFormalGroup_WittPointFamilyInt94 lines · statements of 2 theoremsDef_MvFormalGroup_OfFormalGroupV2387 lines · statements of 1 theorems
Deformations 18 modules
Def_Deformations_MatrixRepresentation24 lines · statements of 24 theoremsDef_Deformations_ConjQuotSubfunctor99 lines · statements of 12 theoremsDef_Deformations_ProartinianCat248 lines · statements of 6 theorems · adapted from upstreamDef_Deformations_ProartinianCompact84 lines · statements of 3 theorems · adapted from upstreamDef_Deformations_TameDescent15 lines · statements of 3 theoremsDef_Deformations_TraceAlgebra126 lines · statements of 3 theoremsDef_Deformations_LiftFunctor71 lines · statements of 2 theorems · adapted from upstreamDef_Deformations_LocalSplitting29 lines · statements of 2 theoremsDef_Deformations_TangentSubmodule107 lines · statements of 2 theoremsDef_Deformations_TaylorWilesLocal29 lines · statements of 2 theoremsDef_Deformations_ClosedSubalgebra262 lines · statements of 1 theoremsDef_Deformations_IsProartinian259 lines · statements of 1 theorems · adapted from upstreamDef_Deformations_MvPowerSeriesObj127 lines · statements of 1 theorems · adapted from upstreamDef_Deformations_ContinuousSMulDiscrete42 lines · statements of 0 theorems · adapted from upstreamDef_Deformations_Deformations_Lemmas310 lines · statements of 0 theorems · adapted from upstreamDef_Deformations_DualNumbers76 lines · statements of 0 theoremsDef_Deformations_Frobenius89 lines · statements of 0 theorems · adapted from upstreamDef_Deformations_IsResidueAlgebra90 lines · statements of 0 theorems · adapted from upstream
FreyPackage 17 modules
Def_FreyPackage_ModMCarrier_Rescale177 lines · statements of 10 theoremsDef_FreyPackage_LevelRaising48 lines · statements of 6 theoremsDef_FreyPackage_EigenformResidualAttachment43 lines · statements of 5 theoremsDef_FreyPackage_RouteAReversePinSeam31 lines · statements of 5 theoremsDef_FreyPackage_IsConductorLevel43 lines · statements of 4 theoremsDef_FreyPackage_LoweringAtUniform64 lines · statements of 3 theoremsDef_FreyPackage_ModMCarrier_OldSublattice117 lines · statements of 3 theoremsDef_FreyPackage_EigenformRealizationSupplyField46 lines · statements of 2 theoremsDef_FreyPackage_MazurAttachmentApparatus92 lines · statements of 2 theoremsDef_FreyPackage_AtPNewLowering28 lines · statements of 1 theoremsDef_FreyPackage_MazurEichlerShimuraFamily30 lines · statements of 1 theoremsDef_FreyPackage_MazurPrincipleAtPStep17 lines · statements of 1 theoremsDef_FreyPackage_DetCyclotomic80 lines · statements of 0 theoremsDef_FreyPackage_ExchangeCase44 lines · statements of 0 theoremsDef_FreyPackage_GaloisRep45 lines · statements of 0 theoremsDef_FreyPackage_LoweringAt51 lines · statements of 0 theoremsDef_FreyPackage_ModMCarrier_LatticeRed35 lines · statements of 0 theorems
TateCurve 15 modules
Def_TateCurve_PointSeries191 lines · statements of 22 theoremsDef_TateCurve_TateParameter634 lines · statements of 19 theoremsDef_TateCurve_TorsionParametrization1,089 lines · statements of 13 theoremsDef_TateCurve_KeystoneVocab251 lines · statements of 10 theoremsDef_TateCurve_XMultIdentities287 lines · statements of 10 theoremsDef_TateCurve_Defect183 lines · statements of 7 theoremsDef_TateCurve_QSeries209 lines · statements of 4 theoremsDef_TateCurve_XMultAlignment332 lines · statements of 3 theoremsDef_TateCurve_Tails91 lines · statements of 2 theoremsDef_TateCurve_DefectLines1,802 lines · statements of 1 theoremsDef_TateCurve_QShift986 lines · statements of 0 theoremsDef_TateCurve_TateFiltrationPrep95 lines · statements of 0 theoremsDef_TateCurve_XMultDistinctRouteB1,453 lines · statements of 0 theoremsDef_TateCurve_XMultSeparation506 lines · statements of 0 theoremsDef_TateCurve_XMultStructure698 lines · statements of 0 theorems
HopfAlgebra 14 modules
Def_HopfAlgebra_CartierDual1,107 lines · statements of 185 theoremsDef_HopfAlgebra_CartierDualInstances50 lines · statements of 77 theoremsDef_HopfAlgebra_HopfKer70 lines · statements of 70 theoremsDef_HopfAlgebra_CartierDualMap135 lines · statements of 53 theoremsDef_HopfAlgebra_FVectStructure161 lines · statements of 22 theoremsDef_HopfAlgebra_CharacterClosure213 lines · statements of 13 theoremsDef_HopfAlgebra_HopfKerHopf596 lines · statements of 11 theoremsDef_HopfAlgebra_HopfOrderData1,117 lines · statements of 8 theoremsDef_HopfAlgebra_RaynaudNormalFormDatum115 lines · statements of 5 theoremsDef_HopfAlgebra_HasFVectDevissage23 lines · statements of 4 theoremsDef_HopfAlgebra_HopfIdealQuotient439 lines · statements of 2 theoremsDef_HopfAlgebra_TorsorGrading84 lines · statements of 2 theoremsDef_HopfAlgebra_HopfTower832 lines · statements of 0 theoremsDef_HopfAlgebra_KummerRadicands62 lines · statements of 0 theorems
M4aHerbrand 13 modules
Def_M4aHerbrand_GenuineDescent104 lines · statements of 531 theoremsDef_M4aHerbrand_SIdeleClassGroup325 lines · statements of 456 theoremsDef_M4aHerbrand_IdeleClassVocab115 lines · statements of 196 theoremsDef_M4aHerbrand_AdeleBaseChange121 lines · statements of 11 theoremsDef_M4aHerbrand_GenuineBeta36 lines · statements of 4 theoremsDef_M4aHerbrand_ArchSemilocal284 lines · statements of 3 theoremsDef_M4aHerbrand_AdeleTopologyFacts110 lines · statements of 1 theoremsDef_M4aHerbrand_FiniteConorm77 lines · statements of 1 theoremsDef_M4aHerbrand_FiniteTensorEquiv384 lines · statements of 0 theorems · adapted from upstreamDef_M4aHerbrand_GenuineTensorEquiv95 lines · statements of 0 theoremsDef_M4aHerbrand_ModuleTopologyBridge148 lines · statements of 0 theoremsDef_M4aHerbrand_OpenMappingBridge76 lines · statements of 0 theoremsDef_M4aHerbrand_SIdeleClassTower197 lines · statements of 0 theorems
GoodReductionJacobian 12 modules
Def_GoodReductionJacobian_RelativeGroupLawBaseChange188 lines · statements of 266 theoremsDef_GoodReductionJacobian_RelativeGroupLawKernel125 lines · statements of 265 theoremsDef_GoodReductionJacobian_BareDeformation54 lines · statements of 96 theoremsDef_GoodReductionJacobian_RelativeGroupLawTranslate128 lines · statements of 70 theoremsDef_GoodReductionJacobian_IsRegluingBy34 lines · statements of 60 theoremsDef_GoodReductionJacobian_RelativeGroupLawAction47 lines · statements of 31 theoremsDef_GoodReductionJacobian_RelativeGroupLawProd355 lines · statements of 18 theoremsDef_GoodReductionJacobian_PartialAction106 lines · statements of 15 theoremsDef_GoodReductionJacobian_RelativeGroupLawAlgPointsV2234 lines · statements of 15 theoremsDef_GoodReductionJacobian_NsmulEigenSubdatum250 lines · statements of 12 theoremsDef_GoodReductionJacobian_RelativeGroupLawKerPair335 lines · statements of 11 theoremsDef_GoodReductionJacobian_RelativeGroupLawFibre140 lines · statements of 6 theorems
EllipticCurve 11 modules
Def_EllipticCurve_FrobeniusTrace67 lines · statements of 291 theoremsDef_EllipticCurve_TateModule884 lines · statements of 189 theoremsDef_EllipticCurve_WeilPairingFun70 lines · statements of 100 theoremsDef_EllipticCurve_ZeroComponentAt23 lines · statements of 43 theoremsDef_EllipticCurve_RubinSilverbergFamily124 lines · statements of 42 theoremsDef_EllipticCurve_FrobeniusEndo58 lines · statements of 21 theoremsDef_EllipticCurve_FunctionFieldPullback1,219 lines · statements of 10 theoremsDef_EllipticCurve_PointReduction35 lines · statements of 6 theoremsDef_EllipticCurve_DivisionPolynomialOmega149 lines · statements of 4 theoremsDef_EllipticCurve_FifteenA138 lines · statements of 3 theoremsDef_EllipticCurve_ValuationInfty185 lines · statements of 1 theorems
CohCarrier 10 modules
Def_CohCarrier_Level507 lines · statements of 172 theoremsDef_CohCarrier_Inst119 lines · statements of 92 theoremsDef_CohCarrier_Lower204 lines · statements of 38 theoremsDef_CohCarrier_LevelPairing108 lines · statements of 35 theoremsDef_CohCarrier_Tower120 lines · statements of 27 theoremsDef_CohCarrier_HeckeData93 lines · statements of 9 theoremsDef_CohCarrier_CharInvolution66 lines · statements of 6 theoremsDef_CohCarrier_SubfamilyHeckeData50 lines · statements of 6 theoremsDef_CohCarrier_Fricke178 lines · statements of 2 theoremsDef_CohCarrier_HeckeDiamondRing58 lines · statements of 1 theorems
Dieudonne 10 modules
Def_Dieudonne_DatumAndHonda87 lines · statements of 108 theoremsDef_Dieudonne_WittVectorHom517 lines · statements of 96 theoremsDef_Dieudonne_WittHomColimit473 lines · statements of 83 theoremsDef_Dieudonne_FontaineHodge380 lines · statements of 45 theoremsDef_Dieudonne_ModpRealization38 lines · statements of 35 theoremsDef_Dieudonne_FontaineFunctor639 lines · statements of 14 theoremsDef_Dieudonne_UnipotentWittCovector569 lines · statements of 13 theoremsDef_Dieudonne_HondaSelfExt91 lines · statements of 9 theoremsDef_Dieudonne_WittGroupHopf442 lines · statements of 1 theoremsDef_Dieudonne_WittKernelHopf422 lines · statements of 1 theorems
LocalLanglands 9 modules
Def_LocalLanglands_HeckeCosetLocal401 lines · statements of 507 theoremsDef_LocalLanglands_HeckeCosetSystem136 lines · statements of 99 theoremsDef_LocalLanglands_HeckePair486 lines · statements of 24 theoremsDef_LocalLanglands_IntegralSubgroupOpen107 lines · statements of 15 theoremsDef_LocalLanglands_LocalHeckeInstance79 lines · statements of 11 theoremsDef_LocalLanglands_CartanDecomposition138 lines · statements of 4 theoremsDef_LocalLanglands_GelfandInvolution160 lines · statements of 1 theoremsDef_LocalLanglands_IntegralSubgroupCompact41 lines · statements of 1 theoremsDef_LocalLanglands_PadicHeckeCosetSystem121 lines · statements of 1 theorems
PDivisibleGroup 9 modules
Def_PDivisibleGroup_Basic324 lines · statements of 199 theoremsDef_PDivisibleGroup_Points449 lines · statements of 170 theoremsDef_PDivisibleGroup_CartierDuality69 lines · statements of 29 theoremsDef_PDivisibleGroup_Dimension84 lines · statements of 24 theoremsDef_PDivisibleGroup_BaseChange192 lines · statements of 18 theoremsDef_PDivisibleGroup_CompletedPoints188 lines · statements of 7 theoremsDef_PDivisibleGroup_Tower425 lines · statements of 6 theoremsDef_PDivisibleGroup_CharacterDifferential97 lines · statements of 5 theoremsDef_PDivisibleGroup_PrimaryTorsion198 lines · statements of 1 theorems
RepTheory 9 modules
Def_RepTheory_SmoothAdmissibleSchurCommutant254 lines · statements of 6 theoremsDef_RepTheory_GL2CongruenceSubgroup532 lines · statements of 3 theoremsDef_RepTheory_LevelDensity28 lines · statements of 1 theoremsDef_RepTheory_TestFunctionActionHom139 lines · statements of 1 theoremsDef_RepTheory_BrauerNesbitt_TraceCharZero454 lines · statements of 0 theoremsDef_RepTheory_MulConvolution105 lines · statements of 0 theoremsDef_RepTheory_SchwartzBruhat_CheckConvolution97 lines · statements of 0 theoremsDef_RepTheory_SmoothVectors322 lines · statements of 0 theoremsDef_RepTheory_TestFunctionAction1,014 lines · statements of 0 theorems
ExtCitation 8 modules
Def_ExtCitation_KummerBridge46 lines · statements of 129 theoremsDef_ExtCitation_LocalLevel_FundamentalClass77 lines · statements of 101 theoremsDef_ExtCitation_LocalLevelResidues697 lines · statements of 45 theorems · adapted from upstreamDef_ExtCitation_AdmissibleExtension_v236 lines · statements of 5 theoremsDef_ExtCitation_CyclotomicUnits69 lines · statements of 4 theoremsDef_ExtCitation_InertiaKummerCharacter244 lines · statements of 3 theoremsDef_ExtCitation_LocalLevelSubgroupsPD74 lines · statements of 2 theoremsDef_ExtCitation_AdmissibleExtension64 lines · statements of 1 theorems
DedekindDomain 7 modules
Def_DedekindDomain_Completion_BaseChange1,160 lines · statements of 237 theorems · adapted from upstreamDef_DedekindDomain_IntegralClosure301 lines · statements of 18 theorems · adapted from upstreamDef_DedekindDomain_AdicValuation_InlineSpecific565 lines · statements of 8 theorems · adapted from upstreamDef_DedekindDomain_FiniteAdeleRing_BaseChange730 lines · statements of 0 theorems · adapted from upstreamDef_DedekindDomain_FiniteAdeleRing_IsDirectLimitRestricted87 lines · statements of 0 theorems · adapted from upstreamDef_DedekindDomain_FiniteAdeleRing_TensorPi231 lines · statements of 0 theorems · adapted from upstreamDef_DedekindDomain_FiniteAdeleRing_TensorRestrictedProduct236 lines · statements of 0 theorems · adapted from upstream
QuaternionAlgebra 7 modules
Def_QuaternionAlgebra_EichlerOrder99 lines · statements of 382 theoremsDef_QuaternionAlgebra_Order60 lines · statements of 113 theoremsDef_QuaternionAlgebra_ReducedNorm44 lines · statements of 106 theoremsDef_QuaternionAlgebra_QMPeriodLattice38 lines · statements of 79 theoremsDef_QuaternionAlgebra_ClassSetHecke245 lines · statements of 39 theoremsDef_QuaternionAlgebra_Order_FiniteIdele66 lines · statements of 3 theoremsDef_QuaternionAlgebra_BaseChange142 lines · statements of 0 theorems
FLTPrelim 6 modules
Def_FLTPrelim_Ramification53 lines · statements of 1,674 theoremsDef_FLTPrelim_Modularity107 lines · statements of 298 theoremsDef_FLTPrelim_GaloisRep84 lines · statements of 174 theorems · adapted from upstreamDef_FLTPrelim_ModularRep119 lines · statements of 119 theoremsDef_FLTPrelim_FreyPackage98 lines · statements of 97 theorems · adapted from upstreamDef_FLTPrelim_CofixedLine21 lines · statements of 17 theorems
LocalNewvector 6 modules
Def_LocalNewvector_AdelicSpanCarrier180 lines · statements of 87 theoremsDef_LocalNewvector_PrincipalSeriesCarrier256 lines · statements of 48 theoremsDef_LocalNewvector_CharConductor126 lines · statements of 30 theoremsDef_LocalNewvector_ReductionFunctor235 lines · statements of 27 theoremsDef_LocalNewvector_ConductorDatum115 lines · statements of 17 theoremsDef_LocalNewvector_CongruenceSubgroupK1167 lines · statements of 2 theorems
ValuationSubring 6 modules
Def_ValuationSubring_ReduceAt305 lines · statements of 172 theoremsDef_ValuationSubring_CompletionDecompositionAction125 lines · statements of 93 theoremsDef_ValuationSubring_CompletionRatClosure53 lines · statements of 93 theoremsDef_ValuationSubring_ResidueValuationSubring57 lines · statements of 4 theoremsDef_ValuationSubring_DecompositionIsometricAut64 lines · statements of 0 theoremsDef_ValuationSubring_RatPlaceCenterHelpers560 lines · statements of 0 theorems · adapted from upstream
DrinfeldCurve 5 modules
Def_DrinfeldCurve_LocalChart40 lines · statements of 444 theoremsDef_DrinfeldCurve_CoordRing365 lines · statements of 281 theoremsDef_DrinfeldCurve_TateRep42 lines · statements of 37 theoremsDef_DrinfeldCurve_FunctionField65 lines · statements of 30 theoremsDef_DrinfeldCurve_MapConstants271 lines · statements of 2 theorems
ModularForm 5 modules
Def_ModularForm_HeckeOperator205 lines · statements of 143 theoremsDef_ModularForm_HeckeOperatorForms113 lines · statements of 64 theoremsDef_ModularForm_AtkinLehnerDatum158 lines · statements of 44 theoremsDef_ModularForm_KatzLevelOne216 lines · statements of 29 theoremsDef_ModularForm_EisensteinChiNegThree28 lines · statements of 15 theorems
MvPolynomial 5 modules
Def_MvPolynomial_CrossingResolutionScheme854 lines · statements of 114 theoremsDef_MvPolynomial_CrossingResolution88 lines · statements of 6 theoremsDef_MvPolynomial_CrossingQuotient69 lines · statements of 4 theoremsDef_MvPolynomial_LogMahlerMeasure162 lines · statements of 4 theoremsDef_MvPolynomial_CrossingResolutionFibrePoints1,483 lines · statements of 1 theorems
FormalGroup 4 modules
Def_FormalGroup_NSeries240 lines · statements of 267 theoremsDef_FormalGroup_DrinfeldBasis64 lines · statements of 229 theoremsDef_FormalGroup_PointTransport47 lines · statements of 174 theoremsDef_FormalGroup_FibreProductGluing320 lines · statements of 0 theorems
FrobeniusDensity 4 modules
Def_FrobeniusDensity_PrimeSums96 lines · statements of 7 theoremsDef_FrobeniusDensity_DegOneAsymptotic45 lines · statements of 3 theoremsDef_FrobeniusDensity_BadPrimes127 lines · statements of 0 theoremsDef_FrobeniusDensity_ClassGroupLSeries36 lines · statements of 0 theorems
HeckeEis 4 modules
Def_HeckeEis_BinaryFormRep141 lines · statements of 84 theoremsDef_HeckeEis_EichlerIntegral150 lines · statements of 32 theoremsDef_HeckeEis_DegeneracyTransfers448 lines · statements of 3 theoremsDef_HeckeEis_Gamma0NebenRep38 lines · statements of 2 theorems
NeronModelInfra 4 modules
Def_NeronModelInfra_TopFormOrder117 lines · statements of 35 theoremsDef_NeronModelInfra_WeakNeronModel163 lines · statements of 31 theoremsDef_NeronModelInfra_OmegaMinimalComponentData214 lines · statements of 14 theoremsDef_NeronModelInfra_SmoothnessDefect109 lines · statements of 9 theorems
Algebra 3 modules
Def_Algebra_PointDerivations65 lines · statements of 106 theoremsDef_Algebra_PatchingDatum45 lines · statements of 30 theoremsDef_Algebra_DescentCofaces81 lines · statements of 4 theorems
ArtinL 3 modules
Def_ArtinL_Abelian232 lines · statements of 31 theoremsDef_ArtinL_EulerFactor120 lines · statements of 12 theoremsDef_ArtinL_Conductor107 lines · statements of 5 theorems
FiniteFlat 3 modules
Def_FiniteFlat_ClosureHopf368 lines · statements of 12 theoremsDef_FiniteFlat_SchematicClosure181 lines · statements of 4 theoremsDef_FiniteFlat_ClosureHopfAlgebra390 lines · statements of 3 theorems
FullLevelTate 3 modules
Def_FullLevelTate_IsoHom229 lines · statements of 6 theoremsDef_FullLevelTate_DrinfeldSpecialization28 lines · statements of 4 theoremsDef_FullLevelTate_Datum68 lines · statements of 0 theorems
HaarMeasure 3 modules
Def_HaarMeasure_HaarChar_AddEquiv361 lines · statements of 0 theorems · adapted from upstreamDef_HaarMeasure_HaarChar_FiniteOrderAutomorphism417 lines · statements of 0 theoremsDef_HaarMeasure_HaarChar_Ring205 lines · statements of 0 theorems · adapted from upstream
HeckeGalois 3 modules
Def_HeckeGalois_EichlerShimura229 lines · statements of 83 theoremsDef_HeckeGalois_MazurCase1BundleNoBT1119 lines · statements of 1 theoremsDef_HeckeGalois_MazurCase1Bundle234 lines · statements of 0 theorems
IsDedekindDomain 3 modules
Def_IsDedekindDomain_FiniteUnitIdelesOutside63 lines · statements of 28 theoremsDef_IsDedekindDomain_FiniteUnitIdeles31 lines · statements of 6 theoremsDef_IsDedekindDomain_SelmerConnectingHom313 lines · statements of 0 theorems
LaurentSeries 3 modules
Def_LaurentSeries_HeckeU51 lines · statements of 11 theoremsDef_LaurentSeries_HeckeV49 lines · statements of 10 theoremsDef_LaurentSeries_XAdic77 lines · statements of 6 theorems
PresheafOfModules 3 modules
Def_PresheafOfModules_InternalHom329 lines · statements of 38 theoremsDef_PresheafOfModules_ExteriorPower200 lines · statements of 29 theoremsDef_PresheafOfModules_PullbackMonoidal531 lines · statements of 5 theorems
CategoryTheory 2 modules
Def_CategoryTheory_OverTotalPresheaf142 lines · statements of 36 theoremsDef_CategoryTheory_Subfunctor_OfIsTerminal23 lines · statements of 0 theorems · adapted from upstream
ClassGroup 2 modules
Def_ClassGroup_GaloisAction203 lines · statements of 2 theoremsDef_ClassGroup_ModP94 lines · statements of 0 theorems
EisensteinGeneral 2 modules
Def_EisensteinGeneral_FactorizationDatum76 lines · statements of 5 theoremsDef_EisensteinGeneral_LocalCorrection79 lines · statements of 3 theorems
EisensteinSeries 2 modules
Def_EisensteinSeries_WeierstrassZeta15 lines · statements of 4 theoremsDef_EisensteinSeries_EisensteinG9 lines · statements of 3 theorems
ExtEndgame 2 modules
Def_ExtEndgame_ProductionDatum86 lines · statements of 140 theoremsDef_ExtEndgame_ChainAdm101 lines · statements of 0 theorems
FieldTheory 2 modules
Def_FieldTheory_RatAlgClosureGalois8 lines · statements of 1 theoremsDef_FieldTheory_RatFuncTower49 lines · statements of 1 theorems
HahnSeries 2 modules
Def_HahnSeries_RamificationBound43 lines · statements of 23 theoremsDef_HahnSeries_Monodromy231 lines · statements of 2 theorems
HeckeModule 2 modules
Def_HeckeModule_IharaRungDatum119 lines · statements of 5 theoremsDef_HeckeModule_IharaDataAt56 lines · statements of 2 theorems
MeasureTheory 2 modules
Def_MeasureTheory_ContractionDecay150 lines · statements of 0 theoremsDef_MeasureTheory_ScalingDichotomy100 lines · statements of 0 theorems
NumberTheory 2 modules
Def_NumberTheory_DedekindSum115 lines · statements of 28 theoremsDef_NumberTheory_DivisorConvolution1,247 lines · statements of 0 theorems
PadicAlgCl 2 modules
Def_PadicAlgCl_RingOfIntegers183 lines · statements of 36 theoremsDef_PadicAlgCl_CyclotomicTower26 lines · statements of 11 theorems
PadicComplex 2 modules
Def_PadicComplex_GaloisAction87 lines · statements of 21 theoremsDef_PadicComplex_TateTrace30 lines · statements of 4 theorems
Patching 2 modules
Def_Patching_SystemTypes59 lines · statements of 12 theorems · adapted from upstreamDef_Patching_CohenMacaulayOfDim24 lines · statements of 1 theorems
RibetLevelLowering 2 modules
Def_RibetLevelLowering_CharacterGroupApparatusV236 lines · statements of 0 theoremsDef_RibetLevelLowering_ExchangeData74 lines · statements of 0 theorems
SheafOfModules 2 modules
Def_SheafOfModules_Monoidal133 lines · statements of 774 theoremsDef_SheafOfModules_MonoidalV2250 lines · statements of 164 theorems
Submodule 2 modules
Def_Submodule_LocalBox118 lines · statements of 173 theoremsDef_Submodule_FiniteAdeleBox79 lines · statements of 56 theorems
TaylorWiles 2 modules
Def_TaylorWiles_Primes107 lines · statements of 25 theoremsDef_TaylorWiles_CyclotomicChar124 lines · statements of 1 theorems
UnramifiedWhittaker 2 modules
Def_UnramifiedWhittaker_HeckeRecursion56 lines · statements of 403 theoremsDef_UnramifiedWhittaker_ZetaIntegrand54 lines · statements of 49 theorems
AbstractHeckeOperator 1 modules
Def_AbstractHeckeOperator153 lines · statements of 0 theorems · adapted from upstream
AdelicDock 1 modules
Def_AdelicDock_LocalEmbedding373 lines · statements of 560 theorems
AdicCompletionGaloisAction 1 modules
Def_AdicCompletionGaloisAction258 lines · statements of 12 theorems
AdicCompletionLocalRing 1 modules
Def_AdicCompletionLocalRing209 lines · statements of 15 theorems
AdicCompletionRestrictScalars 1 modules
Def_AdicCompletionRestrictScalars78 lines · statements of 0 theorems
AdicCompletionRingFunctoriality 1 modules
Def_AdicCompletionRingFunctoriality226 lines · statements of 0 theorems
AdicCompletionTensorRing 1 modules
Def_AdicCompletionTensorRing130 lines · statements of 0 theorems
Analysis 1 modules
Def_Analysis_HalfLineIntercept70 lines · statements of 0 theorems
ArithFrobResidue 1 modules
Def_ArithFrobResidue78 lines · statements of 1 theorems
ClassFunction 1 modules
Def_ClassFunction_Induced213 lines · statements of 2 theorems
Compat 1 modules
Def_Compat_Mathlib430341 lines · statements of 52 theorems
CompletionInvariants 1 modules
Def_CompletionInvariants157 lines · statements of 0 theorems
CuspidalType 1 modules
Def_CuspidalType_IsCuspidalOfType109 lines · statements of 80 theorems
CyclotomicUniv 1 modules
Def_CyclotomicUniv_Base186 lines · statements of 2 theorems
Deformation 1 modules
Def_Deformation_SplitCoordinates196 lines · statements of 9 theorems
DifferentFiltrationFormula 1 modules
Def_DifferentFiltrationFormula92 lines · statements of 2 theorems
DifferentFiltrationMonogenicDischarge 1 modules
Def_DifferentFiltrationMonogenicDischarge104 lines · statements of 0 theorems
DirichletCharacter 1 modules
Def_DirichletCharacter_DirichletIdeleChar189 lines · statements of 11 theorems
DualIsogenyAPI 1 modules
Def_DualIsogenyAPI317 lines · statements of 7 theorems
DualIsogenyExistence 1 modules
Def_DualIsogenyExistence192 lines · statements of 0 theorems
DualSelmer 1 modules
Def_DualSelmer_ExtConditions33 lines · statements of 125 theorems
FormalHecke 1 modules
Def_FormalHecke_Eigensystem19 lines · statements of 5 theorems
FreyCurve 1 modules
Def_FreyCurve_Basic43 lines · statements of 0 theorems · adapted from upstream
Gamma0Away 1 modules
Def_Gamma0Away148 lines · statements of 2 theorems
Gamma0AwayUnitsChar 1 modules
Def_Gamma0AwayUnitsChar89 lines · statements of 1 theorems
Gamma0CoeffCohomology 1 modules
Def_Gamma0CoeffCohomology154 lines · statements of 89 theorems
Gamma0CoeffCohomologyEigen 1 modules
Def_Gamma0CoeffCohomologyEigen113 lines · statements of 44 theorems
Gamma0HeckeOperatorHom 1 modules
Def_Gamma0HeckeOperatorHom305 lines · statements of 57 theorems
Gamma0UnitsChar 1 modules
Def_Gamma0UnitsChar23 lines · statements of 4 theorems
HaarQuotient 1 modules
Def_HaarQuotient36 lines · statements of 141 theorems
HeckeCharacter 1 modules
Def_HeckeCharacter_FiniteOrder31 lines · statements of 44 theorems
IharaAmalgam 1 modules
Def_IharaAmalgam99 lines · statements of 1 theorems
IharaAmalgamMap 1 modules
Def_IharaAmalgamMap154 lines · statements of 2 theorems
IharaGamma0Fin 1 modules
Def_IharaGamma0Fin70 lines · statements of 1 theorems
IharaIota 1 modules
Def_IharaIota189 lines · statements of 13 theorems
IharaLemma 1 modules
Def_IharaLemma_IdempotentSplitting259 lines · statements of 127 theorems
IharaMennickeCarrier 1 modules
Def_IharaMennickeCarrier188 lines · statements of 11 theorems
IncidenceSystem 1 modules
Def_IncidenceSystem261 lines · statements of 4 theorems
IntMatrixOrder 1 modules
Def_IntMatrixOrder_StructureConstants308 lines · statements of 0 theorems
InvariantBaseChange 1 modules
Def_InvariantBaseChange130 lines · statements of 0 theorems
InvariantsCompletion 1 modules
Def_InvariantsCompletion516 lines · statements of 0 theorems
IsLocalRing 1 modules
Def_IsLocalRing_SmallExtensionTangent273 lines · statements of 0 theorems
Isogeny 1 modules
Def_Isogeny_ConditionalCurrency226 lines · statements of 66 theorems
JPSS 1 modules
Def_JPSS_CubicLiftFactor207 lines · statements of 1 theorems
JacJ1 1 modules
Def_JacJ1_ChartAlgebra385 lines · statements of 15 theorems
JacJ1Iface 1 modules
Def_JacJ1Iface138 lines · statements of 1,050 theorems
LatticeTreeBaseChange 1 modules
Def_LatticeTreeBaseChange436 lines · statements of 31 theorems
LatticeTreeOrbital 1 modules
Def_LatticeTreeOrbital2,336 lines · statements of 8 theorems
LinearMap 1 modules
Def_LinearMap_ExtPushout135 lines · statements of 3 theorems
LocalGL2 1 modules
Def_LocalGL2_Kirillov935 lines · statements of 1 theorems
LocalReciprocity 1 modules
Def_LocalReciprocity_IsLocalReciprocityMap32 lines · statements of 1 theorems
LocalRing 1 modules
Def_LocalRing_PrincipalUnits35 lines · statements of 19 theorems
M4aLocalCFT 1 modules
Def_M4aLocalCFT_VocabDefs54 lines · statements of 6 theorems
MDivRepresents 1 modules
Def_MDivRepresents87 lines · statements of 14 theorems
MazurAdmissible 1 modules
Def_MazurAdmissible_GaloisModule80 lines · statements of 14 theorems
ModPForms 1 modules
Def_ModPForms_SSDatum48 lines · statements of 1 theorems
ModelTransfer 1 modules
Def_ModelTransfer_ClearedData285 lines · statements of 3 theorems
Module 1 modules
Def_Module_CommFamilyAnnPart71 lines · statements of 3 theorems
MvPowerSeries 1 modules
Def_MvPowerSeries_RestrictedEvalV2520 lines · statements of 0 theorems
NarrowRayClassGroup 1 modules
Def_NarrowRayClassGroup987 lines · statements of 27 theorems
Nat 1 modules
Def_Nat_MacaulayPow14 lines · statements of 25 theorems
NetPairing 1 modules
Def_NetPairing_Basic100 lines · statements of 0 theorems
NormIndex 1 modules
Def_NormIndex_AdmissibleExpOfDegree80 lines · statements of 27 theorems
PadicInt 1 modules
Def_PadicInt_KummerCarrier110 lines · statements of 4 theorems
PeriodPair 1 modules
Def_PeriodPair_Uniformization145 lines · statements of 16 theorems
Polynomial 1 modules
Def_Polynomial_DeuringPolynomial13 lines · statements of 20 theorems
PolynomialCompletion 1 modules
Def_PolynomialCompletion250 lines · statements of 0 theorems
PowerSeries 1 modules
Def_PowerSeries_FormalHeckeOperators44 lines · statements of 17 theorems
PrimeNormIndex 1 modules
Def_PrimeNormIndex_AdmissibleExpAt53 lines · statements of 3 theorems
ProjectiveLineMatrixAction 1 modules
Def_ProjectiveLineMatrixAction183 lines · statements of 7 theorems
RamificationChain 1 modules
Def_RamificationChain_Wild21 lines · statements of 9 theorems
RatIdele 1 modules
Def_RatIdele_Normalizer392 lines · statements of 305 theorems
Rep 1 modules
Def_Rep_QuotientRightTranslation73 lines · statements of 4 theorems
Representation 1 modules
Def_Representation_AbsolutelyIrreducible34 lines · statements of 12 theorems · adapted from upstream
RingTheory 1 modules
Def_RingTheory_AffineDilatation70 lines · statements of 12 theorems
SchurMultiplierTrivial 1 modules
Def_SchurMultiplierTrivial46 lines · statements of 13 theorems
SemilocalAdicCompletion 1 modules
Def_SemilocalAdicCompletion418 lines · statements of 1 theorems
SmoothOfClosedPoints 1 modules
Def_SmoothOfClosedPoints324 lines · statements of 0 theorems
StabilizerCompletionAction 1 modules
Def_StabilizerCompletionAction88 lines · statements of 0 theorems
Stickelberger 1 modules
Def_Stickelberger_Basic35 lines · statements of 2 theorems
SwdAlgebra 1 modules
Def_SwdAlgebra35 lines · statements of 12 theorems
SymmetricPowerBlockwiseFTSym 1 modules
Def_SymmetricPowerBlockwiseFTSym863 lines · statements of 0 theorems
SymmetricPowerPowerSeriesFTSym 1 modules
Def_SymmetricPowerPowerSeriesFTSym315 lines · statements of 0 theorems
TensorProductDomain 1 modules
Def_TensorProductDomain158 lines · statements of 0 theorems
TwistedNormClasses 1 modules
Def_TwistedNormClasses843 lines · statements of 227 theorems
TwistedUnipotentTerm 1 modules
Def_TwistedUnipotentTerm_SemiLocalOrbitalVocab106 lines · statements of 42 theorems
TwoChartCech 1 modules
Def_TwoChartCech_GluedLines150 lines · statements of 20 theorems
Valuation 1 modules
Def_Valuation_CompletionAlgebra31 lines · statements of 1 theorems