OAI/NumberTheory/SiegelZeros/Structure/
1159 declarations, 0 contain sorry, 0 declared as axioms; 74 files
Files
- AffineAssembly.lean 16 declarations
- AffineFactor.lean 7 declarations
- ArchimedeanTheta.lean 5 declarations
- ArithFrobIntegerGlobalCongruence.lean 2 declarations
- ArithmeticCutoffTransport.lean 33 declarations
- Augmentation.lean 13 declarations
- CanonicalDivisorScalars.lean 25 declarations
- CanonicalGoodMass.lean 8 declarations
- CharacterEstimates.lean 32 declarations
- CodimensionOne.lean 7 declarations
- ComponentHeight.lean 2 declarations
- ConcreteArchimedean.lean 48 declarations
- ConcreteArchimedeanBridge.lean 3 declarations
- ConeMap.lean 38 declarations
- ConeMapEval.lean 3 declarations
- Convergence.lean 5 declarations
- CyclicPrimeFactor.lean 1 declarations
- DegreeMap.lean 39 declarations
- DominantFunctionFieldHom.lean 18 declarations
- DvrFractions.lean 2 declarations
- EndomorphismEulerAdditivity.lean 14 declarations
- EvalOneInvariantJetMonomial.lean 1 declarations
- EventuallyInputs.lean 4 declarations
- Factorization.lean 5 declarations
- FiberCount.lean 2 declarations
- FieldAutomorphisms.lean 59 declarations
- FiniteLower.lean 3 declarations
- FiniteTypeFieldModelEquiv.lean 38 declarations
- FinrankDegreePiecePosPrimeVariableNotMem.lean 4 declarations
- FinsuppCandidates.lean 3 declarations
- GaussFixedField.lean 41 declarations
- GaussLegendre.lean 3 declarations
- GenericCombination.lean 4 declarations
- GradedGeneration.lean 8 declarations
- HeightFourIdentity.lean 4 declarations
- Homogenize.lean 31 declarations
- IdealPowLayer.lean 26 declarations
- IdentityHeight.lean 19 declarations
- InvariantJetLinearMap.lean 33 declarations
- InvariantJetMonomial.lean 12 declarations
- IteratedKoszulExactness.lean 3 declarations
- KoszulDualInitial.lean 9 declarations
- KoszulDualStep.lean 37 declarations
- KoszulTopTerm.lean 5 declarations
- LaurentEvalOne.lean 29 declarations
- LinearShearHom.lean 45 declarations
- LinearVariableBasis.lean 23 declarations
- MapIInfPrimesOver.lean 1 declarations
- MasterContradiction.lean 11 declarations
- MultiplicityCycles.lean 28 declarations
- NotEventuallyMaster.lean 27 declarations
- OmegaIndependence.lean 5 declarations
- OrderedBasis.lean 10 declarations
- PrimeCutBudget.lean 9 declarations
- PrimeDegreeExistence.lean 2 declarations
- QuadraticAdjoinBasis.lean 32 declarations
- QuadraticEigencharacter.lean 20 declarations
- QuadraticEigencharacterAutCongr.lean 3 declarations
- Radicand.lean 4 declarations
- RamifiedMass.lean 7 declarations
- RealBridge.lean 6 declarations
- RealCutoff.lean 3 declarations
- RectangleGenerators.lean 47 declarations
- RectanglePresentation.lean 14 declarations
- RectangleThreshold.lean 52 declarations
- RectangularGradedPieceGeneratedByDegreeOne.lean 1 declarations
- SelectedComponentTaylor.lean 35 declarations
- SignedDiscriminant.lean 9 declarations
- SplitClosedPointCompatibility.lean 3 declarations
- SqrtTwoField.lean 16 declarations
- SumCardFilterSumMin.lean 3 declarations
- SumLogDivFilterDvdTwoMul.lean 14 declarations
- SumLogPrimeFactors.lean 20 declarations
- ThetaJetBridge.lean 5 declarations