OAI/NumberTheory/Jacobsthal/Siegel/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 20 imports below, so a file that imports it gets all of them.
Imports
- OAI.NumberTheory.Jacobsthal.Siegel.BiquadraticBasisGroupTransport
- OAI.NumberTheory.Jacobsthal.Siegel.ClosureSpecMapZeroLocus
- OAI.NumberTheory.Jacobsthal.Siegel.CompletedLAnalyticOrderNeTop
- OAI.NumberTheory.Jacobsthal.Siegel.DegreeSliceQuotientEquiv
- OAI.NumberTheory.Jacobsthal.Siegel.DirichletRealZeroBoundProof
- OAI.NumberTheory.Jacobsthal.Siegel.Divisibility
- OAI.NumberTheory.Jacobsthal.Siegel.FractionEquivAlgebra
- OAI.NumberTheory.Jacobsthal.Siegel.FractionEulerDerivation
- OAI.NumberTheory.Jacobsthal.Siegel.GlobalPivotValuationExponent
- OAI.NumberTheory.Jacobsthal.Siegel.LogarithmicFormLemma
- OAI.NumberTheory.Jacobsthal.Siegel.MapIInfPrimesOver
- OAI.NumberTheory.Jacobsthal.Siegel.NormLogDerivLFunctionNegLogDerivZeta
- OAI.NumberTheory.Jacobsthal.Siegel.NormalizedHomogeneousChartEquation
- OAI.NumberTheory.Jacobsthal.Siegel.PivotBounds
- OAI.NumberTheory.Jacobsthal.Siegel.RectangularGradedPieceGeneratedByDegreeOne
- OAI.NumberTheory.Jacobsthal.Siegel.SumCardFilterSumMin
- OAI.NumberTheory.Jacobsthal.Siegel.SumCharacterPeriodZero
- OAI.NumberTheory.Jacobsthal.Siegel.TorusImmersionGenericPointFormallySmooth
- OAI.NumberTheory.Jacobsthal.Siegel.TorusIntoProj
- OAI.NumberTheory.Jacobsthal.Siegel.TorusJetZeroSchemeInclusion