OAI/Combinatorics/Chromatic/Walls/
2208 declarations, 0 contain sorry, 0 declared as axioms; 214 files
Files
- AdjointExpansion.lean 10 declarations
- AffineCutTelescoping.lean 8 declarations
- AllOrderSectionLine.lean 7 declarations
- Average.lean 10 declarations
- BraidingFiltration.lean 3 declarations
- CenterCoefficientScalarLinear.lean 1 declarations
- CenterLineNaturality.lean 2 declarations
- CenterLineSpecialization.lean 11 declarations
- CenteredUnitRatio.lean 5 declarations
- ChartRefinement.lean 5 declarations
- ComparisonLine.lean 13 declarations
- ComparisonRefinement.lean 12 declarations
- CompleteUnitRecursion.lean 4 declarations
- CompletedBiUnit.lean 3 declarations
- CompletedCutAction.lean 19 declarations
- CompletedInfinityCut.lean 4 declarations
- CompletedInverse.lean 22 declarations
- CompletedPathAction.lean 14 declarations
- CompletedPathIndependence.lean 9 declarations
- CompletedPureComparison.lean 22 declarations
- CoproductSymbol.lean 3 declarations
- CountEmbedding.lean 8 declarations
- CountSumDimension.lean 11 declarations
- DegreeIsolatedReordering.lean 10 declarations
- DirectSumBilinear.lean 2 declarations
- DirectSumSubtype.lean 5 declarations
- ElementaryMatrixDuality.lean 13 declarations
- EulerFiniteProduct.lean 3 declarations
- FilteredDualIndependence.lean 1 declarations
- FilteredTensorComm.lean 5 declarations
- FilteredTensorInsert.lean 2 declarations
- FiltrationHomogeneousRank.lean 9 declarations
- FiniteElementaryAdjoint.lean 16 declarations
- FiniteFiberInfinity.lean 8 declarations
- FiniteFibreFinsupp.lean 6 declarations
- FiniteLatticePairing.lean 30 declarations
- FinitePathPerturbation.lean 7 declarations
- FinitePureMutation.lean 8 declarations
- FiniteRayGeometry.lean 17 declarations
- FiniteRefinementImport.lean 1 declarations
- FiniteRefinementImportAll.lean 10 declarations
- FiniteReorderingEnergy.lean 16 declarations
- FiniteSignCharts.lean 7 declarations
- FiniteStringReordering.lean 17 declarations
- FiniteWallCrossing.lean 8 declarations
- FiniteWallPositive.lean 2 declarations
- ForwardChartMutation.lean 27 declarations
- ForwardInventoryRotation.lean 12 declarations
- ForwardPolynomialMutation.lean 15 declarations
- FourCellFactorization.lean 9 declarations
- GenericAffineProbes.lean 2 declarations
- GenericLineJoining.lean 13 declarations
- GeometricFinitePositive.lean 2 declarations
- GeometricMutationLines.lean 13 declarations
- GlobalWallPositive.lean 12 declarations
- Grade.lean 7 declarations
- GraphBlockPairing.lean 5 declarations
- GraphTriangularEmbedding.lean 7 declarations
- Grid.lean 5 declarations
- HNGeometry.lean 33 declarations
- HNMatrixTriangular.lean 15 declarations
- HNRestrictionOrder.lean 19 declarations
- HNSpanning.lean 31 declarations
- HNTorusFactor.lean 6 declarations
- HalfspaceLaurentTransport.lean 2 declarations
- IncomingDisplacement.lean 5 declarations
- IncomingEquality.lean 27 declarations
- IncomingExtremalLocality.lean 4 declarations
- IncomingRayElement.lean 13 declarations
- IncomingSystem.lean 23 declarations
- IncomingTransportTrace.lean 6 declarations
- IndependentRotationComparison.lean 2 declarations
- InfinityCutCharts.lean 5 declarations
- InfinityFiniteLoop.lean 6 declarations
- InfinityLine.lean 7 declarations
- InfinityPath.lean 11 declarations
- IsolatedPositivePlane.lean 8 declarations
- IsotropicLiteralPositive.lean 9 declarations
- LaurentCompletion.lean 16 declarations
- LaurentCompletionFaithful.lean 5 declarations
- LaurentFiniteDecorations.lean 9 declarations
- LaurentGradedFibers.lean 3 declarations
- LaurentLinearNaturality.lean 2 declarations
- LaurentPolynomialAction.lean 6 declarations
- LaurentPolynomialEnergy.lean 12 declarations
- LaurentPositiveDomination.lean 17 declarations
- LaurentProjectionFormula.lean 1 declarations
- LaurentRayEmbedding.lean 9 declarations
- LaurentScalarAction.lean 1 declarations
- LineOldTransport.lean 11 declarations
- LinearFiltrationBilinear.lean 3 declarations
- LinearFiltrationFinite.lean 1 declarations
- LinearFiltrationOperators.lean 4 declarations
- Mass.lean 14 declarations
- MutatedAnchors.lean 6 declarations
- MutatedHalfspaceTransport.lean 9 declarations
- MutatedIncomingNonpure.lean 1 declarations
- MutatedIncomingNonpureRoot.lean 2 declarations
- MutatedLineCompletion.lean 15 declarations
- MutatedNoCutTransport.lean 8 declarations
- MutatedPathCompletion.lean 13 declarations
- MutatedPathIndependent.lean 12 declarations
- MutatedPureLine.lean 10 declarations
- MutatedWallKernel.lean 6 declarations
- MutationChamberPaths.lean 7 declarations
- MutationEventualIncoming.lean 5 declarations
- MutationIncomingFinite.lean 8 declarations
- MutationIncomingProbes.lean 7 declarations
- MutationInfinityAlgebra.lean 7 declarations
- MutationLaurentCompletion.lean 8 declarations
- MutationLogCompletion.lean 6 declarations
- MutationMonomialAction.lean 6 declarations
- MutationRegradeCompatibility.lean 5 declarations
- MutationSimpleIncoming.lean 12 declarations
- NamedIndependentRotation.lean 1 declarations
- NegativeRayCrossing.lean 5 declarations
- NonpJoint.lean 4 declarations
- OffCutJoint.lean 3 declarations
- OrderedRootReordering.lean 10 declarations
- Pack.lean 26 declarations
- PathOldTransport.lean 8 declarations
- PathRoot.lean 20 declarations
- PlanarJointFactorization.lean 3 declarations
- PlanarRayOrder.lean 6 declarations
- PlanarRefinement.lean 10 declarations
- PolynomialAdjointCoefficients.lean 4 declarations
- PolynomialCoeffLinear.lean 14 declarations
- PolynomialIncomingPerturbation.lean 6 declarations
- PolynomialIncomingProbes.lean 2 declarations
- PolynomialSection.lean 6 declarations
- PowerSeriesThreeFactors.lean 8 declarations
- PrimitiveStrings.lean 16 declarations
- PureActualCoefficients.lean 16 declarations
- PureCutFactorization.lean 7 declarations
- PureCutGroup.lean 8 declarations
- QuantumTorusChartCompletion.lean 16 declarations
- QuantumTorusRaySeries.lean 16 declarations
- QuantumTorusWallLeading.lean 4 declarations
- RationalCocycleExt.lean 3 declarations
- RationalCutIdentity.lean 18 declarations
- RationalFiberReciprocal.lean 18 declarations
- RationalFiberScale.lean 15 declarations
- RationalIntervalModel.lean 2 declarations
- RationalPureCocycle.lean 22 declarations
- RationalReadExt.lean 2 declarations
- RationalTensorDetection.lean 24 declarations
- RayIncomingIdentification.lean 11 declarations
- RayLaurentExpansion.lean 26 declarations
- RealLatticeRealization.lean 37 declarations
- RefinedLaurent.lean 3 declarations
- RefinedTensorDetection.lean 8 declarations
- RootClosureFacts.lean 4 declarations
- RootLaurentCompletion.lean 3 declarations
- RootProducts.lean 26 declarations
- SectionGenericPerturbation.lean 10 declarations
- SectionIncoming.lean 21 declarations
- SectionLineProgram.lean 1 declarations
- SectionRayTransition.lean 11 declarations
- ShuffleFiltration.lean 3 declarations
- ShuffleTensorLinear.lean 10 declarations
- SignedMultiplicity.lean 12 declarations
- SimpleAdjointFiber.lean 13 declarations
- SimpleIncomingData.lean 13 declarations
- SimpleIncomingElement.lean 12 declarations
- SquarefreeBlocks.lean 13 declarations
- StationaryIntegerSequences.lean 37 declarations
- StringPositiveFactor.lean 6 declarations
- StringRay.lean 9 declarations
- StringReorderingEnergy.lean 11 declarations
- StringRootClosure.lean 3 declarations
- StringStrip.lean 21 declarations
- Taylor.lean 18 declarations
- TensorAssociatedGrade.lean 22 declarations
- TensorFiltrationIdeals.lean 2 declarations
- TensorFiltrationInterchange.lean 15 declarations
- TensorGradeFiniteSum.lean 2 declarations
- TensorGradeFunctor.lean 14 declarations
- TensorMiddleFiltration.lean 6 declarations
- TensorPolynomialLinear.lean 2 declarations
- ThresholdWords.lean 11 declarations
- TorusAdjointExpansion.lean 5 declarations
- TorusPositive.lean 17 declarations
- TranslatedCompletion.lean 18 declarations
- TriangularAnchorProjection.lean 11 declarations
- TriangularAnchored.lean 11 declarations
- TriangularCommutativity.lean 8 declarations
- TriangularDirectSum.lean 1 declarations
- TriangularGapOrthogonality.lean 16 declarations
- TriangularGapPairing.lean 17 declarations
- TriangularGapTotals.lean 12 declarations
- TriangularGaps.lean 21 declarations
- TriangularIncoming.lean 6 declarations
- TriangularLateStationarity.lean 14 declarations
- TriangularLevelQueues.lean 21 declarations
- TriangularLinearIncoming.lean 11 declarations
- TriangularLinearSection.lean 16 declarations
- TriangularMonomialCriterion.lean 11 declarations
- TriangularMonomialProducer.lean 3 declarations
- TriangularPeriodTransport.lean 6 declarations
- TriangularPolynomialStationarity.lean 14 declarations
- TriangularPositivePowers.lean 14 declarations
- TriangularScheduledRoots.lean 28 declarations
- TripleSymbols.lean 10 declarations
- TruncatedFactorization.lean 3 declarations
- UnitalCoproductNaturality.lean 15 declarations
- UnitalGradeComparison.lean 8 declarations
- WallLineInitial.lean 7 declarations
- WallRegrade.lean 25 declarations
- WallUnitNegative.lean 14 declarations
- WallUnits.lean 39 declarations
- WeightedCompletion.lean 4 declarations
- WeightedInverseAdjoint.lean 7 declarations
- WeightedRay.lean 7 declarations
- WordLengthFiltration.lean 12 declarations