OAI/NumberTheory/CubicGram/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 44 imports below, so a file that imports it gets all of them.
Imports
- OAI.NumberTheory.CubicGram.Definitions
- OAI.NumberTheory.CubicGram.Coordinates
- OAI.NumberTheory.CubicGram.IntegerBasis
- OAI.NumberTheory.CubicGram.ResidueCharacters
- OAI.NumberTheory.CubicGram.GaussCharacters
- OAI.NumberTheory.CubicGram.EuclideanDomain
- OAI.NumberTheory.CubicGram.PrimeFactors
- OAI.NumberTheory.CubicGram.Conjugation
- OAI.NumberTheory.CubicGram.PrimaryNormalization
- OAI.NumberTheory.CubicGram.SquarefreeGauss
- OAI.NumberTheory.CubicGram.Mobius
- OAI.NumberTheory.CubicGram.Jacobi
- OAI.NumberTheory.CubicGram.ReciprocityKernel
- OAI.NumberTheory.CubicGram.Reciprocity
- OAI.NumberTheory.CubicGram.Periodization
- OAI.NumberTheory.CubicGram.LatticePoisson
- OAI.NumberTheory.CubicGram.FrequencyGauss
- OAI.NumberTheory.CubicGram.PeriodicPoisson
- OAI.NumberTheory.CubicGram.MixedPoisson
- OAI.NumberTheory.CubicGram.GramPoisson
- OAI.NumberTheory.CubicGram.CommonFactors
- OAI.NumberTheory.CubicGram.CubicOperator
- OAI.NumberTheory.CubicGram.MellinDecay
- OAI.NumberTheory.CubicGram.MellinNorm
- OAI.NumberTheory.CubicGram.CubeExtraction
- OAI.NumberTheory.CubicGram.NormRecurrence
- OAI.NumberTheory.CubicGram.LatticeCounts
- OAI.NumberTheory.CubicGram.DyadicRecurrence
- OAI.NumberTheory.CubicGram.CommonRows
- OAI.NumberTheory.CubicGram.GlobalRecurrence
- OAI.NumberTheory.CubicGram.SieveMajorant
- OAI.NumberTheory.CubicGram.SieveBase
- OAI.NumberTheory.CubicGram.FullCubeExtraction
- OAI.NumberTheory.CubicGram.CubeEstimates
- OAI.NumberTheory.CubicGram.SieveExponent
- OAI.NumberTheory.CubicGram.PoissonBounds
- OAI.NumberTheory.CubicGram.QuantitativeRecurrence
- OAI.NumberTheory.CubicGram.SieveImprovement
- OAI.NumberTheory.CubicGram.InnerExtension
- OAI.NumberTheory.CubicGram.GramMellin
- OAI.NumberTheory.CubicGram.GramDyad
- OAI.NumberTheory.CubicGram.GramNormalize
- OAI.NumberTheory.CubicGram.GramCommon
- OAI.NumberTheory.CubicGram.CharacterGram