Machine-generated inventory

Source exposition

A commit-pinned map of checked Lean modules. Declaration-level metadata is available in JSON.

ModuleLinesDeclarations Imports
EllipticCurves.Examples.ExceptionalCubicReduction182180
EllipticCurves.IntegralModel11520
EllipticCurves.Mathlib.AdicCompletionExtension377180
EllipticCurves.Mathlib.AdicFormalGroupLog768420
EllipticCurves.Mathlib.AdicValuation136100
EllipticCurves.Mathlib.Basic1,6311490
EllipticCurves.Mathlib.Chabauty.AdicTopology7260
EllipticCurves.Mathlib.Chabauty.ExpConverge394260
EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Basic314180
EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Invariance670360
EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Log377200
EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Points19670
EllipticCurves.Mathlib.Chabauty.FormalGroupLaw4000
EllipticCurves.Mathlib.Chabauty.LocalRing4920
EllipticCurves.Mathlib.Chabauty.LogIso553280
EllipticCurves.Mathlib.Chabauty.MvPSeries536450
EllipticCurves.Mathlib.Chabauty.MvPowerSeriesComp316280
EllipticCurves.Mathlib.Chabauty.MvPowerSeriesPDeriv362200
EllipticCurves.Mathlib.Chabauty.PSeries324300
EllipticCurves.Mathlib.Chabauty.PadicInt5720
EllipticCurves.Mathlib.Chabauty.PadicValNat6730
EllipticCurves.Mathlib.EllipticCurvePoint148150
EllipticCurves.ReductionAtPrime467320
EllipticCurves.VariableChange2000
EllipticCurves.WeierstrassFormalGroup.Chord1,025830
EllipticCurves.WeierstrassFormalGroup.Eval621550
EllipticCurves.WeierstrassFormalGroup.Filtration969372
EllipticCurves.WeierstrassFormalGroup.Foundations891552
EllipticCurves.WeierstrassFormalGroup.GroupLaw961274
EllipticCurves.WeierstrassFormalGroup.Reduction800504
EllipticCurves.WeierstrassFormalGroup.ThirdPoint704402
EllipticCurves37031
MazurTorsion.Arithmetic.CardinalityReduction6634
MazurTorsion.Arithmetic.ExceptionalProducts10295
MazurTorsion.Arithmetic.ExceptionalTwoTen4852011
MazurTorsion.Arithmetic.ExceptionalTwoTwelve402132
MazurTorsion.Arithmetic.LowTorsionObstructions7485
MazurTorsion.Arithmetic.OddPrimeObstructions9185
MazurTorsion.Arithmetic.OrderTwentyTwentyFour13153
MazurTorsion.Arithmetic.PointOrder237117
MazurTorsion.Arithmetic.PointOrderReduction14776
MazurTorsion.Arithmetic.RankTwoReduction9252
MazurTorsion.EllipticCurve.TwoIsogeny690513
MazurTorsion.EllipticCurve.TwoIsogenyMultiples523162
MazurTorsion.EllipticCurve.TwoTorsionNormalization238152
MazurTorsion.EllipticCurve.VariableChange218170
MazurTorsion.Foundations.DivisionPolynomialDiscriminantFive639543
MazurTorsion.Foundations.DivisionPolynomialDiscriminantSeven1,053683
MazurTorsion.Foundations.DivisionPolynomialRootCriterion656126
MazurTorsion.Foundations.FullFourTorsion37366
MazurTorsion.Foundations.NaiveHeightDescent370218
MazurTorsion.Foundations.OddPrimeFullTorsion480217
MazurTorsion.Foundations.ThreeTorsion536115
MazurTorsion.Foundations.TwoTorsion241128
MazurTorsion.GroupTheory.ClassificationCardinality7870
MazurTorsion.GroupTheory.CyclicKernelExtension9610
MazurTorsion.GroupTheory.FiniteClassification840320
MazurTorsion.GroupTheory.ForbiddenEmbeddings7570
MazurTorsion.GroupTheory.IndependentCyclicGenerators224104
MazurTorsion.GroupTheory.IndexNSmulFG16173
MazurTorsion.GroupTheory.TorsionEquiv6050
MazurTorsion.Kubert.OrderEighteenModel343181
MazurTorsion.Kubert.OrderEighteenReduction13832
MazurTorsion.Kubert.OrderElevenModel384261
MazurTorsion.Kubert.OrderElevenReduction346121
MazurTorsion.Kubert.OrderFifteen4822
MazurTorsion.Kubert.OrderFifteenModel472292
MazurTorsion.Kubert.OrderFifteenReduction22082
MazurTorsion.Kubert.OrderFourteen5122
MazurTorsion.Kubert.OrderFourteenModel466362
MazurTorsion.Kubert.OrderFourteenReduction551221
MazurTorsion.Kubert.OrderNineReduction19651
MazurTorsion.Kubert.OrderSevenCorrespondence10193
MazurTorsion.Kubert.OrderSevenHauptmodul9012
MazurTorsion.Kubert.OrderSevenIsogeny652482
MazurTorsion.Kubert.OrderSevenParametrization14951
MazurTorsion.Kubert.OrderSixteenReduction1,090293
MazurTorsion.Kubert.OrderThirteenModel14191
MazurTorsion.Kubert.OrderThirteenReduction452131
MazurTorsion.Kubert.OrderThirtyFive1501
MazurTorsion.Kubert.OrderTwentyFive1501
MazurTorsion.Kubert.OrderTwentyOne8933
MazurTorsion.Kubert.OrderTwentyOneExceptionalJ185102
MazurTorsion.Kubert.OrderTwentyOneReduction18133
MazurTorsion.Kubert.OrderTwentySeven5722
MazurTorsion.Kubert.OrderTwentySevenEndpoint10061
MazurTorsion.Kubert.OrderTwentySevenLegChunks35,4531,9551
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.DenominatorCube9151
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.DenominatorSquare3821
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCube21115
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps0To713981
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps16To2314181
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps24To3114481
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps32To358441
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps32To401402
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps36To4010351
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorCubeSteps8To1514081
MazurTorsion.Kubert.OrderTwentySevenLegStagesA.NumeratorSquare8351
MazurTorsion.Kubert.OrderTwentySevenLegStagesA1604
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Bands0To514561
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Bands12To1714361
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Bands18To238261
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Bands6To1116661
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.DenominatorNonzero8951
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.KernelCubic2711
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.MNum3415
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.MNumFour6114
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.MNumOne17212
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.MNumThree8714
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.MNumTwo9314
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Scalars4441
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TOne5812
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TOneSteps0To48551
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TOneSteps5To99351
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TTwo8112
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TTwoSteps0To611871
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TTwoSteps10To137941
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TTwoSteps7To131402
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.TTwoSteps7To96631
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WOneX8012
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WOneXSteps0To28531
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WOneXSteps3To58931
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WTwoX9012
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WTwoXSteps0To18521
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WTwoXSteps2To49731
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WZeroX5211
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.WZeroXSteps9641
MazurTorsion.Kubert.OrderTwentySevenLegStagesB.Zero2,238645
MazurTorsion.Kubert.OrderTwentySevenLegStagesB1603
MazurTorsion.Kubert.OrderTwentySevenLegStagesC127101
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.Bezout4221
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.BigIdentity7419
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.CoefficientPowers4541
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.DenominatorPowers6951
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.NumeratorDenominator5031
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.NumeratorDenominatorSquare7751
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.WeightOne7441
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.WeightZero5131
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.WeightsHigh5741
MazurTorsion.Kubert.OrderTwentySevenLegStagesD.ZeroSum4111
MazurTorsion.Kubert.OrderTwentySevenLegStagesD1902
MazurTorsion.Kubert.OrderTwentySevenLegs104111
MazurTorsion.Kubert.OrderTwentySevenReduction17952
MazurTorsion.Kubert.OrderTwentySevenThirdLeg8452
MazurTorsion.Kubert.OrderTwentySevenTrisection398131
MazurTorsion.Kubert.TateNormalForm376146
MazurTorsion.Kubert.TateNormalFormMultiples15291
MazurTorsion.Kubert.ThreeNormalForm222111
MazurTorsion.NumberTheory.ExceptionalCubicDescent1,1845610
MazurTorsion.NumberTheory.ExceptionalCubicReduction4222
MazurTorsion.NumberTheory.ExceptionalQuarticDescent511103
MazurTorsion.NumberTheory.FermatCubicClassification10521
MazurTorsion.NumberTheory.QuarticDifferenceDescent340131
MazurTorsion.NumberTheory.RatNorthcott6120
MazurTorsion.NumberTheory.RationalRootsOfUnity4120
MazurTorsion.NumberTheory.SevenAdicCertificates11966
MazurTorsion.NumberTheory.XOneEighteenDescent626552
MazurTorsion.NumberTheory.XOneEighteenFiniteField429523
MazurTorsion.NumberTheory.XOneElevenDescent551354
MazurTorsion.NumberTheory.XOneElevenReduction321302
MazurTorsion.NumberTheory.XOneFifteenDescent1,530661
MazurTorsion.NumberTheory.XOneFifteenReduction559383
MazurTorsion.NumberTheory.XOneFourteenDescent1,145571
MazurTorsion.NumberTheory.XOneFourteenReduction224172
MazurTorsion.NumberTheory.XOneThirteenDescent986892
MazurTorsion.NumberTheory.XOneThirteenFiniteField286403
MazurTorsion.NumberTheory.XZeroFortyNineDescent1,306515
MazurTorsion.NumberTheory.XZeroFortyNineReduction233152
MazurTorsion.NumberTheory.XZeroFortyNineTransfer53283
MazurTorsion.NumberTheory.XZeroTwentyOneDescent7603718
MazurTorsion.NumberTheory.XZeroTwentyOneRankZero1,236596
MazurTorsion.NumberTheory.XZeroTwentyOneReduction413232
MazurTorsion.NumberTheory.XZeroTwentyOneTransfer577142
MazurTorsion.NumberTheory.XZeroTwentySevenClassification1,443833
MazurTorsion95089