OAI/NumberTheory/SiegelZeros/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 21 imports below, so a file that imports it gets all of them.
Imports
- OAI.NumberTheory.SiegelZeros.Characters.BiquadraticBasisGroupTransport
- OAI.NumberTheory.SiegelZeros.Characters.DirichletRealZeroBoundProof
- OAI.NumberTheory.SiegelZeros.Characters.NormLogDerivLFunctionNegLogDerivZeta
- OAI.NumberTheory.SiegelZeros.Characters.SumCharacterPeriodZero
- OAI.NumberTheory.SiegelZeros.Conclusions.Theorem
- OAI.NumberTheory.SiegelZeros.Determinants.Divisibility
- OAI.NumberTheory.SiegelZeros.Differentials.FractionEulerDerivation
- OAI.NumberTheory.SiegelZeros.EntireFunctions.ClosureSpecMapZeroLocus
- OAI.NumberTheory.SiegelZeros.EntireFunctions.CompletedLAnalyticOrderNeTop
- OAI.NumberTheory.SiegelZeros.EntireFunctions.LogarithmicFormLemma
- OAI.NumberTheory.SiegelZeros.EntireFunctions.TorusJetZeroSchemeInclusion
- OAI.NumberTheory.SiegelZeros.Hilbert.NormalizedHomogeneousChartEquation
- OAI.NumberTheory.SiegelZeros.Intersection.TorusImmersionGenericPointFormallySmooth
- OAI.NumberTheory.SiegelZeros.Intersection.TorusIntoProj
- OAI.NumberTheory.SiegelZeros.LocalAlgebra.DegreeSliceQuotientEquiv
- OAI.NumberTheory.SiegelZeros.LocalAlgebra.FractionEquivAlgebra
- OAI.NumberTheory.SiegelZeros.Selection.GlobalPivotValuationExponent
- OAI.NumberTheory.SiegelZeros.Selection.PivotBounds
- OAI.NumberTheory.SiegelZeros.Structure.MapIInfPrimesOver
- OAI.NumberTheory.SiegelZeros.Structure.RectangularGradedPieceGeneratedByDegreeOne
- OAI.NumberTheory.SiegelZeros.Structure.SumCardFilterSumMin