OAI/Combinatorics/PolynomialVacuum/Algebra/
3227 declarations, 0 contain sorry, 0 declared as axioms; 134 files
Files
- AllFinalCupZeros.lean 3 declarations
- AllSizeConstruction.lean 12 declarations
- AllSizeInduction.lean 3 declarations
- AnalyticNormalization.lean 4 declarations
- AnalyticResolvent.lean 9 declarations
- BaseBounds.lean 31 declarations
- BaseEndpoints.lean 8 declarations
- BaseGrading.lean 14 declarations
- BaseNatural.lean 7 declarations
- BasePolynomials.lean 13 declarations
- BaseThree.lean 84 declarations
- BaseThreeNode.lean 28 declarations
- BaseTwo.lean 33 declarations
- BilinearChannels.lean 12 declarations
- BitCoefficients.lean 19 declarations
- BitRigidity.lean 4 declarations
- BitRigidityTarget.lean 3 declarations
- BraidEndomorphisms.lean 12 declarations
- BraidTrain.lean 8 declarations
- Candidate.lean 11 declarations
- CandidateEndpoints.lean 5 declarations
- ChargeCombinatorics.lean 5 declarations
- ChargeStep.lean 11 declarations
- CupDivisibility.lean 12 declarations
- CupPointwiseSlide.lean 4 declarations
- CupPrescriptions.lean 15 declarations
- CupProductSwap.lean 7 declarations
- CupQuotientBounds.lean 7 declarations
- CupScalarCompatibility.lean 6 declarations
- CupSlide.lean 86 declarations
- CupSlidePolynomial.lean 8 declarations
- CupSurface.lean 11 declarations
- CupSurfaceInterpolation.lean 5 declarations
- CupTransport.lean 9 declarations
- CyclicBounds.lean 4 declarations
- CyclicCups.lean 5 declarations
- DiscrepancyRoots.lean 5 declarations
- EmptyNonzero.lean 1 declarations
- ExchangeDegrees.lean 10 declarations
- ExchangeDifference.lean 6 declarations
- ExchangeDiscrepancy.lean 6 declarations
- ExchangeDiscrepancyBounds.lean 3 declarations
- Existence.lean 2 declarations
- FinalCupZeros.lean 6 declarations
- FinalExchange.lean 2 declarations
- FiniteLift.lean 5 declarations
- FiniteTranslation.lean 10 declarations
- FirstCupInterpolation.lean 5 declarations
- FirstCupNodeAssembly.lean 5 declarations
- FirstCupNodes.lean 3 declarations
- FirstCupPolynomial.lean 3 declarations
- FirstCupRegularNode.lean 3 declarations
- FirstCupZeroNode.lean 6 declarations
- FirstExchanges.lean 4 declarations
- FullCyclicity.lean 1 declarations
- FusionScalars.lean 6 declarations
- Gram.lean 18 declarations
- HomogeneityStep.lean 6 declarations
- HomogeneousCupSlide.lean 84 declarations
- HomogeneousCupUnslide.lean 84 declarations
- HomogeneousYangBaxter.lean 759 declarations
- InhomogeneousCircuit.lean 19 declarations
- InhomogeneousRow.lean 4 declarations
- InsertionSlide.lean 246 declarations
- InterpolatedCups.lean 3 declarations
- InterpolatedDegrees.lean 2 declarations
- InterpolatedExchanges.lean 3 declarations
- InterpolatedZero.lean 7 declarations
- Interpolation.lean 1 declarations
- InterpolationDefinitions.lean 2 declarations
- InterpolationNodes.lean 3 declarations
- KillSite.lean 9 declarations
- LagrangeClearing.lean 11 declarations
- LagrangeDegree.lean 8 declarations
- LastDegrees.lean 1 declarations
- LastPolynomial.lean 7 declarations
- MarkedDegree.lean 6 declarations
- NaturalCandidateEndpoints.lean 3 declarations
- NaturalCollision.lean 5 declarations
- NaturalCovariance.lean 6 declarations
- NaturalCup.lean 10 declarations
- NaturalMarkLeft.lean 4 declarations
- NaturalParameters.lean 10 declarations
- NaturalRotation.lean 19 declarations
- NaturalUncup.lean 3 declarations
- NaturalUnitary.lean 3 declarations
- NodeFactors.lean 9 declarations
- NodesUniqueness.lean 4 declarations
- NormalizedCyclic.lean 2 declarations
- PairImage.lean 5 declarations
- PartialCupScalar.lean 4 declarations
- PenultimateCup.lean 3 declarations
- PolynomialGenericity.lean 5 declarations
- PolynomialScalars.lean 58 declarations
- PolynomialScaling.lean 8 declarations
- PolynomialSlice.lean 7 declarations
- PrescriptionCollision.lean 5 declarations
- PrescriptionCovariance.lean 5 declarations
- PrescriptionDegree.lean 3 declarations
- PrescriptionEvaluation.lean 5 declarations
- Projectors.lean 20 declarations
- QuotientExchange.lean 8 declarations
- QuotientRigidity.lean 4 declarations
- RegularInterpolation.lean 4 declarations
- Ring.lean 0 declarations
- RowCircuit.lean 19 declarations
- RowEigenvector.lean 9 declarations
- Scalars.lean 18 declarations
- ScaledRootGuard.lean 5 declarations
- ScalingTensors.lean 10 declarations
- SpectatorDegree.lean 6 declarations
- SpectatorFiltration.lean 8 declarations
- SpectatorList.lean 5 declarations
- SpectralAnalytic.lean 12 declarations
- SpectralEigenvector.lean 13 declarations
- Table.lean 83 declarations
- Target.lean 25 declarations
- TensorActions.lean 14 declarations
- TensorYangBaxter.lean 4 declarations
- ThreeSiteRestriction.lean 15 declarations
- TraceClosing.lean 9 declarations
- TraceTrain.lean 13 declarations
- TrainEvaluation.lean 8 declarations
- TransportCovariance.lean 1 declarations
- TransportFiltration.lean 6 declarations
- Triangularity.lean 6 declarations
- TrilinearRigidity.lean 13 declarations
- TripleActions.lean 14 declarations
- TripleBitRigidity.lean 6 declarations
- Unitary.lean 6 declarations
- VectorBilinear.lean 12 declarations
- YangBaxter.lean 759 declarations
- ZeroFiltration.lean 8 declarations
- ZeroSpectatorPair.lean 5 declarations