OAI/Combinatorics/Chromatic/GradedAlgebra/
890 declarations, 0 contain sorry, 0 declared as axioms; 105 files
Files
- BiRegrade.lean 9 declarations
- BoundedWordLaurent.lean 7 declarations
- CenterCoefficientMembership.lean 1 declarations
- ClearedSeparation.lean 5 declarations
- CompleteUnit.lean 13 declarations
- ConvolutionPostcomposition.lean 2 declarations
- CovectorFactor.lean 5 declarations
- CutoffRow.lean 3 declarations
- DHomogeneous.lean 2 declarations
- DegreeSet.lean 7 declarations
- ElementaryExpressionBounds.lean 3 declarations
- EnergyLaurentFinite.lean 4 declarations
- EnergyLaurentSeries.lean 13 declarations
- EnergyLimit.lean 21 declarations
- Eval.lean 19 declarations
- FiniteCovectorPerturbation.lean 6 declarations
- FinitelySupportedUnitRows.lean 17 declarations
- FintypeEnergyProduct.lean 4 declarations
- GradedBuilders.lean 3 declarations
- GradedFormalLog.lean 3 declarations
- HNSeries.lean 11 declarations
- HalfspacePolynomialCoefficients.lean 11 declarations
- HomogeneousBasisFibre.lean 5 declarations
- HomogeneousElementaryExpressions.lean 15 declarations
- HomogenizedPolynomialSection.lean 8 declarations
- InputOrderedProduct.lean 10 declarations
- IntegerHomogeneous.lean 2 declarations
- KernelTraceLog.lean 20 declarations
- LaurentAffineCancellation.lean 4 declarations
- LaurentBiTruncation.lean 7 declarations
- LaurentConstantMultiplication.lean 2 declarations
- LaurentContinuity.lean 28 declarations
- LaurentDeshear.lean 19 declarations
- LaurentFilteredMultiplication.lean 1 declarations
- LaurentGeometric.lean 19 declarations
- LaurentHomogenize.lean 7 declarations
- LaurentInfinity.lean 24 declarations
- LaurentMapNaturality.lean 2 declarations
- LaurentProductNaturality.lean 1 declarations
- LaurentPureAction.lean 13 declarations
- LaurentRectangularKernel.lean 13 declarations
- LaurentRegrade.lean 26 declarations
- LaurentRegradeFinite.lean 4 declarations
- LaurentRegradePure.lean 2 declarations
- LaurentScalarNaturality.lean 2 declarations
- LaurentSigns.lean 3 declarations
- LaurentUnitSigns.lean 1 declarations
- MutatedEndpoint.lean 4 declarations
- MutatedNoCutCone.lean 5 declarations
- MutatedPureFace.lean 4 declarations
- MutationCoordinates.lean 9 declarations
- MutationDegreeBound.lean 7 declarations
- MutationLaurentTransport.lean 4 declarations
- MutationOrientedCompatibility.lean 3 declarations
- MutationRootMap.lean 17 declarations
- NilpotentLogarithm.lean 26 declarations
- NilpotentSeriesInverse.lean 1 declarations
- NoncommExpand.lean 7 declarations
- NoncommSeriesCalculus.lean 12 declarations
- NonpHomogenize.lean 16 declarations
- NonpRegrade.lean 16 declarations
- NonpRegradeFaithful.lean 13 declarations
- PowerSeriesProductLeading.lean 4 declarations
- PowerSeriesSplit.lean 13 declarations
- PowerSeriesSplitLeading.lean 14 declarations
- Product.lean 9 declarations
- ProjectionRecursion.lean 1 declarations
- PureCoefficient.lean 2 declarations
- PureComparisonIdentification.lean 19 declarations
- PureFaceLog.lean 6 declarations
- PurePolynomialCoefficients.lean 4 declarations
- QuantumTorusAlgebra.lean 4 declarations
- QuantumTorusSignFactors.lean 8 declarations
- RationalCenteredAction.lean 6 declarations
- RationalLaurentFaithful.lean 13 declarations
- RationalLaurentScalars.lean 19 declarations
- RationalPolynomialDivisibility.lean 15 declarations
- RationalPureCoefficients.lean 8 declarations
- RationalRegrade.lean 8 declarations
- RationalShearCocycle.lean 16 declarations
- RationalShearEmbedding.lean 3 declarations
- RealRootCoordinates.lean 4 declarations
- RegradeLog.lean 10 declarations
- RootCoefficientLocality.lean 3 declarations
- RootCoefficients.lean 3 declarations
- RootMutationInventory.lean 7 declarations
- RootSectionHalfspace.lean 8 declarations
- RootTruncation.lean 15 declarations
- RotationLocalPolynomials.lean 6 declarations
- SeriesApproximation.lean 13 declarations
- SimpleBinomial.lean 9 declarations
- SplitContinuity.lean 9 declarations
- SquarefreeCoefficient.lean 3 declarations
- Strict.lean 3 declarations
- StringBackshift.lean 4 declarations
- StringStripSeries.lean 5 declarations
- SupportedConvolution.lean 9 declarations
- TraceLogDerivative.lean 3 declarations
- TruncatedChart.lean 2 declarations
- TruncatedPrecisionClosure.lean 11 declarations
- UnitIndexEnergy.lean 8 declarations
- UnitSelectionLaurent.lean 6 declarations
- UnitalProduct.lean 6 declarations
- WeightedPushTwist.lean 3 declarations
- WeightedTorusSeries.lean 17 declarations