`OAI/RingTheory/Multiplicity/`

4262 declarations, 0 contain sorry, 0 declared as axioms; 278 files

Files

ActualCechTranspose.lean 31 declarations
AdditiveLength.lean 2 declarations
AdicDense.lean 3 declarations
AdicFlatCriterion.lean 8 declarations
AlgebraicResidueTensor.lean 6 declarations
AlternatingCechAlt.lean 47 declarations
AlternatingCechPost.lean 54 declarations
AlternatingCechPrismPrimitive.lean 57 declarations
AlternatingCechUnaugmentedComplex.lean 59 declarations
ArbitraryCoefficientField.lean 11 declarations
ArtinianSupport.lean 2 declarations
AssociatedGradedReduction.lean 9 declarations
BicomplexEuler.lean 3 declarations
BicomplexImageLift.lean 11 declarations
CarrierOperators.lean 18 declarations
CartierQuotientDevissage.lean 7 declarations
CartierTowerDevissage.lean 6 declarations
CechCarrierOperators.lean 18 declarations
CechCartierRange.lean 5 declarations
CechCartierZRange.lean 5 declarations
CechCopies.lean 14 declarations
CechExact.lean 8 declarations
CechIndexing.lean 4 declarations
CechNormalization.lean 24 declarations
CechNormalizationRows.lean 21 declarations
CechProducts.lean 8 declarations
CechReduction.lean 12 declarations
CharPModuleLength.lean 1 declarations
CoefficientFieldLocalSection.lean 15 declarations
CompleteNoetherian.lean 1 declarations
CompleteQuotient.lean 2 declarations
CompleteResidueExtension.lean 4 declarations
ComplexConductor.lean 6 declarations
ComplexEstimate.lean 2 declarations
ComplexEstimateAllModule.lean 1 declarations
ComplexReduction.lean 4 declarations
ComplexTensorComparison.lean 6 declarations
ComplexTheorem.lean 3 declarations
ContractibleRetract.lean 2 declarations
CyclicDutta.lean 7 declarations
DuttaAlgClosed.lean 1 declarations
DuttaBaseChange.lean 5 declarations
DuttaData.lean 8 declarations
DuttaDimensionZero.lean 3 declarations
DuttaDomain.lean 3 declarations
DuttaEstimateLimit.lean 1 declarations
DuttaEulerLimit.lean 3 declarations
DuttaFrobeniusShift.lean 4 declarations
DuttaInfinitePerfect.lean 1 declarations
DuttaMinimalEstimate.lean 1 declarations
DuttaPerfectResidue.lean 3 declarations
DuttaPerfectionValue.lean 1 declarations
ElementaryContractibleProjector.lean 7 declarations
ExactSequenceTransport.lean 2 declarations
ExceptionalCoefficientSquare.lean 16 declarations
ExceptionalFibre.lean 20 declarations
ExceptionalFibreRestriction.lean 4 declarations
ExceptionalRootCohomology.lean 14 declarations
ExceptionalRootEulerZ.lean 3 declarations
FibreSquare.lean 10 declarations
FieldNilpotentLift.lean 19 declarations
FilteredCechAugmentationRing.lean 37 declarations
FilteredCechAugmented.lean 39 declarations
FilteredFractionReesDenominator.lean 43 declarations
FilteredFractionReesDenominatorTheory.lean 41 declarations
FiniteComplexTopInclusion.lean 52 declarations
FiniteFreeRetract.lean 3 declarations
FiniteFreeTensorCohomology.lean 6 declarations
FiniteGradedQuotient.lean 4 declarations
FiniteLengthPrimary.lean 1 declarations
FiniteModuleCech.lean 14 declarations
FiniteModuleTensor.lean 7 declarations
FiniteTensorBound.lean 3 declarations
FlatLocalSupport.lean 3 declarations
FrobeniusComplexStage.lean 6 declarations
FrobeniusFiniteLength.lean 7 declarations
FrobeniusHomologyFinite.lean 6 declarations
FrobeniusHomologyGrowth.lean 5 declarations
FrobeniusHomologySmall.lean 3 declarations
FrobeniusIntermediatePowerMap.lean 37 declarations
FrobeniusModule.lean 3 declarations
FrobeniusOrderTransfer.lean 2 declarations
FrobeniusScalarError.lean 3 declarations
FrobeniusTensorStage.lean 2 declarations
FrobeniusTensorTransfer.lean 1 declarations
GradedChartCochains.lean 47 declarations
GradedLineBasisHasBasis.lean 51 declarations
GradedLinearNormalization.lean 3 declarations
HomogeneousEval.lean 5 declarations
HomogeneousFunctor.lean 11 declarations
HomogeneousRegradeIdentity.lean 49 declarations
HomogeneousZeroPiece.lean 5 declarations
HomologyLengthDevissage.lean 2 declarations
IdealFilteredComplex.lean 19 declarations
IdealFilteredHomotopy.lean 4 declarations
IdealFilteredLayers.lean 7 declarations
IdealFilteredQuotient.lean 7 declarations
IdealFilteredRows.lean 6 declarations
IdealGradedLengthPiece.lean 29 declarations
IdealGradedRing.lean 44 declarations
IdealQuotientFunctor.lean 12 declarations
IntermediateTensorLength.lean 1 declarations
KoszulConeFunctor.lean 23 declarations
KoszulFiniteComplexBound.lean 2 declarations
KoszulHomologyMap.lean 38 declarations
KoszulPowerGrowth.lean 4 declarations
KoszulQuotientFinite.lean 7 declarations
KoszulSwap.lean 20 declarations
KoszulTensorSingle.lean 18 declarations
LechBoundedEquiv.lean 54 declarations
LechCokernelComp.lean 35 declarations
LechConnectingIso.lean 48 declarations
LechFactorizationMap.lean 44 declarations
LechFiniteFree.lean 14 declarations
LechHilbertSerre.lean 18 declarations
LechHomogeneousEval.lean 59 declarations
LechHomologyProp.lean 6 declarations
LechLengthLe.lean 20 declarations
LechLevel.lean 48 declarations
LechMapCochain.lean 26 declarations
LechNatTrans.lean 23 declarations
LechPiIso.lean 44 declarations
LechQuotientScalar.lean 32 declarations
LechSignedUnit.lean 45 declarations
LechTorsionOf.lean 62 declarations
LinearNormalization.lean 10 declarations
LinearNormalizationDimension.lean 3 declarations
LocalContractibility.lean 10 declarations
Main.lean 1 import, no declarations
MinimalComplex.lean 5 declarations
MinimalComplexReduction.lean 3 declarations
MinimalReduction.lean 6 declarations
ModuleComplexQuotient.lean 8 declarations
NativeDescentCanonicalAlg.lean 41 declarations
NonminimalPivot.lean 2 declarations
NormalizationModuleLimit.lean 1 declarations
NormalizedLengthTrivialRelation.lean 29 declarations
NumericalSupport.lean 37 declarations
OrderedRootBasis.lean 6 declarations
PartialLaurentTotalDegree.lean 58 declarations
PerfectDomainStagesTensorTo.lean 29 declarations
PerfectTensorLimit.lean 3 declarations
PerfectionAcyclicity.lean 1 declarations
PerfectionModuleLengthFinite.lean 2 declarations
PowerSeriesFinDimension.lean 29 declarations
PowerSeriesFlatVariables.lean 11 declarations
PrimeFiltrationEuler.lean 3 declarations
PrimeFiltrationMultiplicity.lean 2 declarations
PrimeFiltrationSupport.lean 37 declarations
PrimeQuotientParameters.lean 1 declarations
PrimitiveChartFaithfullyFlat.lean 49 declarations
PrincipalCoverRegularRegularMap.lean 74 declarations
ProductSourceCoverAllowedEmpty.lean 60 declarations
ProductSourceCoverCechNat.lean 52 declarations
ProductSourceCoverFaceSlice.lean 65 declarations
ProductSourceCoverHighThreshold.lean 33 declarations
ProductSourceCoverOrdinaryPositive.lean 53 declarations
ProductSourceCoverRootSigned.lean 37 declarations
ProjectiveGhost.lean 4 declarations
ProjectiveReduction.lean 10 declarations
PureProjective.lean 7 declarations
QuotientExtension.lean 2 declarations
QuotientParameters.lean 1 declarations
QuotientShort.lean 5 declarations
ReducedRootCohomology.lean 9 declarations
ReductionMultiplicity.lean 3 declarations
ReesCoordinate.lean 5 declarations
ReesExceptionalRing.lean 19 declarations
ReesExceptionalSquare.lean 13 declarations
ReesRegular.lean 7 declarations
ReesRootBundle.lean 15 declarations
ReesRootCech.lean 13 declarations
ReesRootCechEuler.lean 6 declarations
ReesRootEuler.lean 11 declarations
ReesRootEulerConstant.lean 2 declarations
ReesRootEulerFunction.lean 3 declarations
ReesRootEulerPositivity.lean 3 declarations
ReesRootEulerRank.lean 2 declarations
ReesRootG.lean 8 declarations
ReesRootGLayer.lean 10 declarations
ReesRootGLayerCohomology.lean 10 declarations
ReesRootInclusion.lean 17 declarations
ReesRootIteration.lean 6 declarations
ReesRootLayerCech.lean 5 declarations
ReesRootLayerTotal.lean 6 declarations
ReesRootLayers.lean 11 declarations
ReesRootMap.lean 15 declarations
ReesRootNilpotence.lean 14 declarations
ReesRootPermutation.lean 5 declarations
ReesRootPositivity.lean 9 declarations
ReesRootPowerPath.lean 8 declarations
ReesRootQuotient.lean 9 declarations
ReesRootQuotientEuler.lean 9 declarations
ReesRootRows.lean 2 declarations
ReesRootThickeningEuler.lean 15 declarations
ReesRootUnfiltered.lean 8 declarations
ReesUlrichCech.lean 10 declarations
ResidueExtension.lean 2 declarations
RestrictedPolynomialImageCechComparisonHomology.lean 44 declarations
RobertsNormalization.lean 1 declarations
RobertsOrderTransfer.lean 2 declarations
RobertsPerfectResidue.lean 1 declarations
RobertsSeparable.lean 3 declarations
RootBaseProjective.lean 4 declarations
RootBundleChartsDenominator.lean 49 declarations
RootCechCoefficients.lean 8 declarations
RootCechProjective.lean 10 declarations
RootChartAtlasGlobalCoefficient.lean 49 declarations
RootChartUlrich.lean 8 declarations
RootCoactionT.lean 60 declarations
RootCoefficientEuler.lean 9 declarations
RootCoordinateMultiplication.lean 3 declarations
RootFibreCech.lean 9 declarations
RootHomogeneousCoordinates.lean 2 declarations
RootInvariantsWeightZero.lean 36 declarations
RootLineEuler.lean 16 declarations
RootOverlap.lean 29 declarations
RootPermutation.lean 18 declarations
RootProjectiveEuler.lean 9 declarations
RootRestriction.lean 11 declarations
RootSectionBase.lean 5 declarations
RootSectionDiagram.lean 11 declarations
RootStageQuotient.lean 9 declarations
RootStripComplement.lean 5 declarations
RootTowerLengthEq.lean 34 declarations
RootTowerNormalizedLength.lean 19 declarations
RootTowerRemainderExponent.lean 56 declarations
RootTowerRootWeight.lean 46 declarations
RootTwist.lean 8 declarations
RootUlrichModule.lean 6 declarations
RootUlrichNaturality.lean 7 declarations
RootUlrichSpan.lean 12 declarations
ScalarCartierLift.lean 8 declarations
ScalarCechComparison.lean 3 declarations
ScalarCechEuler.lean 4 declarations
ScalarCechShift.lean 11 declarations
ScalarChartComparison.lean 8 declarations
ScalarExtensionComplexCompare.lean 5 declarations
ScalarExtensionDepth.lean 6 declarations
ScalarExtensionFiniteHomology.lean 1 declarations
ScalarExtensionHomotopy.lean 5 declarations
ScalarHomologyError.lean 10 declarations
ScalarQuotientTransport.lean 3 declarations
SeparableOrderNormalizedLength.lean 31 declarations
ShortRankEuler.lean 2 declarations
SignedCechBicRow.lean 33 declarations
SourceGradedCechHomology.lean 45 declarations
SourceGradedThickeningNat.lean 56 declarations
StandardFactorChartsL.lean 47 declarations
SubalgebraStageFromBase.lean 35 declarations
SumEstimate.lean 2 declarations
SymmetricAffine.lean 6 declarations
TensorCechEuler.lean 11 declarations
TensorCechHomotopy.lean 3 declarations
TensorCechRankEuler.lean 4 declarations
TensorCoefficientFibre.lean 3 declarations
TensorConductor.lean 11 declarations
TensorEuler.lean 8 declarations
TensorGeneratorBound.lean 4 declarations
TensorIdealRange.lean 3 declarations
TensorPushout.lean 6 declarations
TensorQuotientCommutation.lean 3 declarations
TensorReduction.lean 2 declarations
TensorRingTwist.lean 5 declarations
TensorTotalHomologyProperty.lean 45 declarations
TorsionAcyclicity.lean 1 declarations
TorsionChartKernel.lean 5 declarations
TorsionScalarComparison.lean 1 declarations
TorsionTensorLeft.lean 3 declarations
TorsionThickening.lean 8 declarations
TorsionZeroStability.lean 8 declarations
TotalExact.lean 8 declarations
TotalGhostRowHom.lean 33 declarations
TowerRestrictedLength.lean 14 declarations
TraceConductorPerfectOrder.lean 29 declarations
TwistedLocalizationPieceMap.lean 41 declarations
UniversalFactorMapMapChart.lean 45 declarations
ZeroHomologyScalarExtension.lean 3 declarations