OAI/NumberTheory/PiExponent/LocalAlgebra/
1122 declarations, 0 contain sorry, 0 declared as axioms; 172 files
Files
- AffineClosedPointLocalization.lean 25 declarations
- AffineIdealSections.lean 8 declarations
- AffineLocalRegularBezout.lean 4 declarations
- AffinePrimeDimensionBridge.lean 1 declarations
- AffineResidueTranscendence.lean 6 declarations
- AffineTranscendenceDimension.lean 5 declarations
- AssociatedPrimeAvoidance.lean 1 declarations
- ClosedPointLocalDimension.lean 3 declarations
- CoherentExtFiniteness.lean 8 declarations
- CoherentInverseFinite.lean 4 declarations
- ColonHilbertStep.lean 5 declarations
- CompleteIntersectionComponentBound.lean 5 declarations
- CompleteIntersectionHilbert.lean 7 declarations
- ComponentMultiplicityBound.lean 1 declarations
- ComponentMultiplicitySum.lean 3 declarations
- ConeComplex.lean 7 declarations
- ConeEquationLength.lean 4 declarations
- ConeLocalLength.lean 42 declarations
- ConePrimeLocalization.lean 11 declarations
- ConeQuotientAugmentation.lean 3 declarations
- ConeRegularSequence.lean 7 declarations
- CoordinateBasisSplitting.lean 9 declarations
- CoordinateContactBound.lean 5 declarations
- CoordinateFiniteSlice.lean 19 declarations
- CoordinateSliceLength.lean 20 declarations
- CoordinateTranscendenceBasis.lean 15 declarations
- CoordinateTranscendenceLocalization.lean 4 declarations
- CumulativeHilbertSections.lean 8 declarations
- CyclicPrimeFactor.lean 1 declarations
- DVRValuationUnique.lean 7 declarations
- Dimension.lean 16 declarations
- EquidimensionalRetainedCut.lean 3 declarations
- FibreContact.lean 7 declarations
- FiltrationLength.lean 3 declarations
- FiniteFreeExtTransfer.lean 3 declarations
- FiniteFreeResolutionExt.lean 8 declarations
- FiniteFromClosedFibers.lean 1 declarations
- FiniteGlobalPresentation.lean 21 declarations
- FiniteSupportLocalIso.lean 5 declarations
- FinsuppCandidates.lean 3 declarations
- FlatLocalLength.lean 4 declarations
- FreeResolutionAssociatedHeight.lean 8 declarations
- GenericCombination.lean 4 declarations
- GlobalInvertibleIdeal.lean 9 declarations
- HilbertDenominatorReduction.lean 2 declarations
- HilbertDifferenceDegree.lean 5 declarations
- HilbertGrowthComparison.lean 3 declarations
- HilbertMultiplicityFiltration.lean 6 declarations
- HilbertZeroVariables.lean 3 declarations
- IdealFiniteGenerators.lean 1 declarations
- IdealModule.lean 25 declarations
- IdealModuleRestriction.lean 6 declarations
- IdealPowerAnnihilator.lean 7 declarations
- IdealPowerDescent.lean 4 declarations
- IdealPowerFiltration.lean 16 declarations
- IdealPowerRestriction.lean 7 declarations
- IdealPullbackMap.lean 6 declarations
- IdealPullbackOpenSquare.lean 6 declarations
- IdealSectionRestriction.lean 11 declarations
- IdealTensorPowers.lean 7 declarations
- IntegralAffineOpenDimension.lean 10 declarations
- InvertibleIdealAway.lean 8 declarations
- InvertibleIdealLocal.lean 16 declarations
- IsolatedIntersectionSteps.lean 7 declarations
- IteratedKoszulExactness.lean 3 declarations
- KoszulBounded.lean 5 declarations
- KoszulDualBottom.lean 8 declarations
- KoszulDualCone.lean 5 declarations
- KoszulDualEndpoint.lean 1 declarations
- KoszulDualInitial.lean 6 declarations
- KoszulDualStep.lean 4 declarations
- KoszulDualTransport.lean 2 declarations
- KoszulFiniteFree.lean 10 declarations
- KoszulTopAugmentation.lean 3 declarations
- KoszulTopTerm.lean 5 declarations
- LocalBezout.lean 1 declarations
- LocalComponentDegree.lean 6 declarations
- LocalIntersectionDimensionOne.lean 3 declarations
- LocalIntersectionExactStep.lean 2 declarations
- LocalIntersectionFormula.lean 4 declarations
- LocalIntersectionLength.lean 12 declarations
- LocalIntersectionMinimalSum.lean 2 declarations
- LocalIntersectionPrimeFactors.lean 5 declarations
- LocalIntersectionPrimeFiltration.lean 3 declarations
- LocalIntersectionQuotientTransport.lean 6 declarations
- LocalIntersectionTransport.lean 8 declarations
- LocalLength.lean 5 declarations
- LocalLengthTransport.lean 5 declarations
- LocalPrefixCutDimension.lean 2 declarations
- LocalPrimeTower.lean 4 declarations
- LocalPullbackSectionOrder.lean 4 declarations
- LocalSectionOrder.lean 10 declarations
- LocalizationQuotientParameters.lean 29 declarations
- LocalizedAlgebraEvaluation.lean 5 declarations
- LocalizedComponent.lean 2 declarations
- LocalizedCyclicFactor.lean 3 declarations
- LocalizedFiltrationLength.lean 1 declarations
- LocalizedLengthEquivalence.lean 4 declarations
- LocalizedMinimalPrimeFamily.lean 5 declarations
- LocalizedOneCutPropagation.lean 4 declarations
- LocalizedRadical.lean 1 declarations
- MultiplicityCycles.lean 5 declarations
- NaturalMultiplicityPropagation.lean 4 declarations
- OpenIsoFunctionField.lean 6 declarations
- OrdinaryMultiplicity.lean 6 declarations
- PairResolutionShortComplex.lean 5 declarations
- ParameterCombinations.lean 4 declarations
- ParameterKilledFiniteLength.lean 8 declarations
- ParameterResidueField.lean 5 declarations
- PointLengthEquiv.lean 5 declarations
- PositiveCoherentExtFiniteness.lean 3 declarations
- PositiveDimensionalHilbert.lean 17 declarations
- PresentedIdealIso.lean 8 declarations
- PrimeCutBudget.lean 6 declarations
- PrimeDegreeExistence.lean 2 declarations
- PrimeFrameMultiplicity.lean 1 declarations
- PrimeHilbertComparison.lean 5 declarations
- PrimeHilbertDegree.lean 7 declarations
- PrimeHilbertDimension.lean 4 declarations
- PrimeHypersurfaceDimension.lean 5 declarations
- PrimeHypersurfaceEquidimension.lean 1 declarations
- PrimeNormalKernel.lean 3 declarations
- PrimeNormalRigidity.lean 7 declarations
- PrimeResidueAlgebraEquiv.lean 6 declarations
- PrimeWeightedBezout.lean 1 declarations
- PrincipalQuotientDimension.lean 2 declarations
- QuotientLengthEquivalence.lean 2 declarations
- QuotientLocalizedLength.lean 5 declarations
- QuotientPrimeResidueBasis.lean 6 declarations
- QuotientSections.lean 5 declarations
- RamifiedLocalLength.lean 4 declarations
- RamifiedLocalization.lean 3 declarations
- RamifiedPointMap.lean 6 declarations
- RamifiedPowerLength.lean 8 declarations
- RegularCutHistory.lean 9 declarations
- RegularDegreePositivity.lean 5 declarations
- RegularHilbertStep.lean 5 declarations
- RegularPairExtObstruction.lean 2 declarations
- RegularParameterAvoidance.lean 3 declarations
- RegularParameterSelection.lean 4 declarations
- RegularParameterSelection2.lean 3 declarations
- RegularPrefixLocalization.lean 2 declarations
- RegularPrefixes.lean 6 declarations
- RegularSequenceAugmentation.lean 5 declarations
- RegularSequenceDualExactness.lean 2 declarations
- RegularSequenceExt.lean 9 declarations
- RegularSequenceExtObstruction.lean 9 declarations
- RegularSequenceHomZero.lean 2 declarations
- RegularSequenceLowExt.lean 4 declarations
- RegularSequenceQuotientTail.lean 8 declarations
- RegularSequenceResolution.lean 8 declarations
- RetainedIntersectionCycles.lean 26 declarations
- RetainedMinimalPrimeFamily.lean 9 declarations
- SectionImageIdeal.lean 11 declarations
- SectionZeroIdeal.lean 4 declarations
- SeparablePointLength.lean 19 declarations
- SerreDimensionShift.lean 5 declarations
- SplitClosedPointCompatibility.lean 3 declarations
- SplitCoordinateClosedPoint.lean 11 declarations
- StabilizedColonPowers.lean 9 declarations
- SubquotientLength.lean 4 declarations
- TensorIdealInclusion.lean 9 declarations
- TranscendenceBasisReduction.lean 1 declarations
- TriangularLocalParameters.lean 24 declarations
- TriangularLocalParametersAssembly.lean 1 declarations
- TriangularLocalParametersTransport.lean 3 declarations
- TwistLocalExtension.lean 2 declarations
- TwistLocalSections.lean 1 declarations
- WeightedBezout.lean 19 declarations
- WeightedBezoutBound.lean 8 declarations
- WeightedChartRingEvaluation.lean 8 declarations
- WeightedLocalLattice.lean 7 declarations