OAI/NumberTheory/SiegelZeros/LocalAlgebra/
1115 declarations, 0 contain sorry, 0 declared as axioms; 69 files
Files
- AffineClosedPointLocalization.lean 34 declarations
- AffineProjChartPolynomialEquiv.lean 4 declarations
- AffineResidueTranscendence.lean 6 declarations
- AlgebraMapMemSpanImage.lean 2 declarations
- BoxPolynomials.lean 12 declarations
- CanonicalQuotient.lean 7 declarations
- CoeffPolynomialEvalMul.lean 2 declarations
- CoefficientLocalizationMaximal.lean 25 declarations
- CoefficientSubspaceEquiv.lean 20 declarations
- ColonSeriesTelescope.lean 7 declarations
- ConePrimeLocalization.lean 72 declarations
- ConeQuotientAugmentation.lean 11 declarations
- ConeRegularSequence.lean 11 declarations
- CoordinateLocalizedPrime.lean 31 declarations
- CoordinateQuotientGrading.lean 30 declarations
- DVRLocalCoordinates.lean 21 declarations
- DegreeSliceQuotientEquiv.lean 8 declarations
- FinrankSpanAlgebraMapImage.lean 4 declarations
- FractionEquivAlgebra.lean 13 declarations
- GaussMinimalPolynomial.lean 8 declarations
- GenericRegularity.lean 4 declarations
- GenericResidueFunctionField.lean 7 declarations
- GlobalStalkExtension.lean 11 declarations
- GradedIdealQuotient.lean 7 declarations
- GreedyPivotsRingEquiv.lean 2 declarations
- HeightFourLength.lean 25 declarations
- JetCoefficients.lean 12 declarations
- LocalFractionAlgebra.lean 24 declarations
- LocalGap.lean 2 declarations
- LocalLength.lean 5 declarations
- LocalQuotientEquiv.lean 35 declarations
- LocalResidueTaylor.lean 5 declarations
- LocalizedFiltrationLength.lean 17 declarations
- LocalizedOneCutPropagation.lean 4 declarations
- LocalizedRadical.lean 3 declarations
- MonicSMulRegularQuotientMapC.lean 21 declarations
- NormalizationPresentationLocalEquiv.lean 35 declarations
- ParameterChoices.lean 7 declarations
- ParameterCombinations.lean 4 declarations
- ParameterIdeal.lean 28 declarations
- ParameterIntegration.lean 7 declarations
- ParameterKilledFiniteLength.lean 8 declarations
- PolynomialBox.lean 38 declarations
- PolynomialBridge.lean 4 declarations
- PolynomialCoefficientLocalization.lean 17 declarations
- PolynomialCumulative.lean 10 declarations
- PolynomialLaurent.lean 30 declarations
- PolynomialLinearCoefficients.lean 37 declarations
- PolynomialLocalRegularParameters.lean 5 declarations
- PrimeResidueAlgebraEquiv.lean 6 declarations
- QuotientPrimeResidueBasis.lean 6 declarations
- RectangularLocalization.lean 12 declarations
- RegularCutHistory.lean 9 declarations
- RegularParameterSelection.lean 11 declarations
- RegularParameterSelectionLemmas.lean 45 declarations
- RegularPrefixLocalization.lean 44 declarations
- RegularSequenceAugmentation.lean 5 declarations
- RegularSequenceSeries.lean 10 declarations
- ResidueDirectionSelection.lean 39 declarations
- ResidueField.lean 10 declarations
- ResidueIndependence.lean 6 declarations
- ResidueMap.lean 26 declarations
- ResidueTensorQuotientAlgEquiv.lean 14 declarations
- RingLength.lean 8 declarations
- ScalarExtension.lean 4 declarations
- SelectedLengthContradiction.lean 29 declarations
- SequenceParameters.lean 2 declarations
- StabilizedColonPowers.lean 9 declarations
- TriangularLocalParametersTransport.lean 78 declarations