OAI/NumberTheory/Jacobsthal/Siegel/
1700 declarations, 0 contain sorry, 0 declared as axioms; 105 files
Files
- AffineProjChartPolynomialEquiv.lean 4 declarations
- AffineZeroScheme.lean 37 declarations
- AlgebraMapMemSpanImage.lean 2 declarations
- ArithFrobIntegerGlobalCongruence.lean 2 declarations
- AuxiliarySqrtPairCharacterField.lean 1 declarations
- BiquadraticArithmeticFull.lean 13 declarations
- BiquadraticBasis.lean 30 declarations
- BiquadraticBasisGroupTransport.lean 7 declarations
- BiquadraticGoodPrimeUnramified.lean 1 declarations
- BiquadraticGoodPrimeUnramifiedSameWitnessEquiv.lean 1 declarations
- BiquadraticThetaMap.lean 3 declarations
- CharacterGlobalGreedyDeterminantFullLocalBounds.lean 1 declarations
- CharacterGlobalGreedyDeterminantMasterBounds.lean 1 declarations
- ClosureSpecMapZeroLocus.lean 5 declarations
- CoeffPolynomialEvalMul.lean 2 declarations
- CoefficientSubspaceEquiv.lean 20 declarations
- CompletedLAnalyticOrderNeTop.lean 18 declarations
- ConductorCompletedL.lean 36 declarations
- ConeChartHomogeneousLocal.lean 4 declarations
- ConeMap.lean 38 declarations
- ConeMapEval.lean 3 declarations
- ConeProjectivePoint.lean 19 declarations
- CoordinateLocalizedPrime.lean 31 declarations
- DegreeMap.lean 39 declarations
- DegreeSliceQuotientEquiv.lean 8 declarations
- DerivationJet.lean 39 declarations
- DirichletRealZeroBound.lean 1 declarations
- DirichletRealZeroBoundProof.lean 1 declarations
- Divisibility.lean 1 declarations
- DominantFunctionFieldHom.lean 18 declarations
- E.lean 32 declarations
- EvalOneInvariantJetMonomial.lean 1 declarations
- FiniteTypeFieldModelEquiv.lean 38 declarations
- FinrankDegreePiecePosPrimeVariableNotMem.lean 4 declarations
- FinrankDerivationCardTranscendenceBasis.lean 16 declarations
- FinrankSpanAlgebraMapImage.lean 4 declarations
- FractionEquivAlgebra.lean 13 declarations
- FractionEulerDerivation.lean 18 declarations
- FrobeniusRetainedCharacterField.lean 1 declarations
- GenericNormalization.lean 36 declarations
- GlobalPivotValuationExponent.lean 2 declarations
- GlobalRectanglePivotBounds.lean 1 declarations
- GlobalWeightSortedJetEquiv.lean 4 declarations
- GradedIdealQuotient.lean 7 declarations
- GreedyPivots.lean 39 declarations
- GreedyPivotsRingEquiv.lean 2 declarations
- GreedyPivotsWeightLowSpan.lean 8 declarations
- HilbertSeries.lean 30 declarations
- HomogeneousDeformation.lean 45 declarations
- Homogenize.lean 31 declarations
- IdealPowLayer.lean 26 declarations
- IntegerCharacter.lean 27 declarations
- IntegralDeterminantTransport.lean 1 declarations
- InvariantDerivation.lean 20 declarations
- InvariantJetLinearMap.lean 33 declarations
- InvariantJetMonomial.lean 12 declarations
- JetRowAutCongr.lean 1 declarations
- LaurentEvalOne.lean 29 declarations
- LinearShearHom.lean 45 declarations
- LinearVariableBasis.lean 23 declarations
- LocalFractionAlgebra.lean 24 declarations
- LocalLengthMulProjectiveClosureDegree.lean 1 declarations
- LocalQuotientEquiv.lean 35 declarations
- LocalizeInvariantDerivationLogCoordinate.lean 2 declarations
- LogarithmicForm.lean 21 declarations
- LogarithmicFormLemma.lean 1 declarations
- Main.lean 20 imports, no declarations
- MapIInfPrimesOver.lean 1 declarations
- MellinConvergentTopIndicator.lean 29 declarations
- MonicSMulRegularQuotientMapC.lean 21 declarations
- NormLogDerivLFunctionNegLogDerivZeta.lean 7 declarations
- NormSqReal.lean 20 declarations
- NormalizationPresentationLocalEquiv.lean 35 declarations
- NormalizedHomogeneousChartEquation.lean 6 declarations
- NormalizedMasterBound.lean 1 declarations
- NotEventuallyMaster.lean 27 declarations
- ParameterIdeal.lean 28 declarations
- PivotBounds.lean 1 declarations
- PolynomialBox.lean 38 declarations
- PolynomialLaurent.lean 30 declarations
- PolynomialLinearCoefficients.lean 37 declarations
- QuadraticAdjoinBasis.lean 32 declarations
- QuadraticEigencharacter.lean 20 declarations
- QuadraticEigencharacterAutCongr.lean 3 declarations
- QuadraticGroupCharacterFrobenius.lean 1 declarations
- RealLogDerivConductorCompletedLDivisorTsum.lean 29 declarations
- RealZeroUniformMasterBound.lean 1 declarations
- RectangleThreshold.lean 52 declarations
- RectangularGradedPieceGeneratedByDegreeOne.lean 1 declarations
- ResidueTensorQuotientAlgEquiv.lean 14 declarations
- RestrictWeightSortedEquiv.lean 22 declarations
- SqrtPairFrobeniusDirections.lean 29 declarations
- SqrtTwoField.lean 16 declarations
- SumCardFilterSumMin.lean 3 declarations
- SumCharacterPeriodZero.lean 34 declarations
- SumLogDivFilterDvdTwoMul.lean 14 declarations
- SumLogPrimeFactors.lean 20 declarations
- TorusDerivationOverRat.lean 16 declarations
- TorusEvalOne.lean 40 declarations
- TorusImmersionGenericPointFormallySmooth.lean 1 declarations
- TorusIntoProj.lean 4 declarations
- TorusJetZeroSchemeInclusion.lean 16 declarations
- TorusQuotientDimensionPosCotangentFinrankThree.lean 9 declarations
- TorusRectangleJetIdealParametersProjectiveDegreeBound.lean 1 declarations
- WeightedJetIndices.lean 22 declarations