OAI/Topology/ArtinGroups/Harmonic/
1430 declarations, 0 contain sorry, 0 declared as axioms; 217 files
Files
- AllEligibleLower.lean 5 declarations
- ArtinAction.lean 4 declarations
- ArtinActionWordArtin.lean 4 declarations
- ArtinReindex.lean 14 declarations
- BinaryProductBoundary.lean 6 declarations
- Block.lean 18 declarations
- BottomWordNil.lean 2 declarations
- Candidate.lean 5 declarations
- CandidateBlockNonpos.lean 2 declarations
- CandidateCapped.lean 1 declarations
- CanonicalFusionLow.lean 8 declarations
- CanonicalFusionLowCount.lean 1 declarations
- CanonicalFusionLowExpansion.lean 1 declarations
- CanonicalFusionMultiplicity.lean 4 declarations
- CanonicalLowSupport.lean 2 declarations
- CappedCandidate.lean 5 declarations
- CappedReflectedHigh.lean 1 declarations
- CartanCommutingZero.lean 5 declarations
- CartanPairingSymm.lean 5 declarations
- Characteristic.lean 13 declarations
- CharacteristicSaturatedInterior.lean 3 declarations
- ConeAttachmentRel.lean 16 declarations
- Contradiction.lean 1 declarations
- Coset.lean 12 declarations
- CosetBelow.lean 14 declarations
- CosetExteriorCap.lean 4 declarations
- CosetOrbit.lean 7 declarations
- CosetOrbitCap.lean 1 declarations
- CosetProfile.lean 4 declarations
- CosetSignUpperTie.lean 4 declarations
- CosetSum.lean 7 declarations
- CosetVectorNullPatch.lean 3 declarations
- CosetVertex.lean 17 declarations
- Crossing.lean 8 declarations
- DimensionNonneg.lean 4 declarations
- DimensionPosMultiplicityPos.lean 5 declarations
- Earlier.lean 10 declarations
- EarlierLinkSubtypeIso.lean 2 declarations
- EarlierLower.lean 13 declarations
- EarlierLowerOrderIso.lean 4 declarations
- EarlierUpper.lean 16 declarations
- EarlyDelay.lean 7 declarations
- EigenvectorProportional.lean 2 declarations
- Eligible.lean 8 declarations
- EligibleFactor.lean 4 declarations
- EligibleLeftNonempty.lean 4 declarations
- EligibleWithin.lean 10 declarations
- Extend.lean 13 declarations
- FamilySocleFiniteTermination.lean 1 declarations
- FiniteArtinPositiveLeft.lean 1 declarations
- FiniteChainEnum.lean 7 declarations
- FiniteFusionEdge.lean 10 declarations
- FinsuppMapDomainFiber.lean 1 declarations
- FoldedCartan.lean 2 declarations
- FoldedSphericalPos.lean 2 declarations
- FrameFamily.lean 11 declarations
- FrameFamilyCapTop.lean 2 declarations
- FrameFamilyTopProportional.lean 2 declarations
- FusionColorRegion.lean 7 declarations
- FusionColorWord.lean 6 declarations
- FusionExpandedWordAction.lean 1 declarations
- FusionExpandedWordPerm.lean 1 declarations
- FusionExpressionAction.lean 2 declarations
- FusionExpressionOrbit.lean 4 declarations
- FusionFactorStep.lean 11 declarations
- FusionFold.lean 11 declarations
- FusionIntegralCartan.lean 6 declarations
- FusionLabel.lean 14 declarations
- FusionOrbitCapMove.lean 1 declarations
- FusionOrbitColorSecondary.lean 2 declarations
- FusionOrbitColorSubobject.lean 1 declarations
- FusionOrbitColorTop.lean 2 declarations
- FusionOrbitModel.lean 8 declarations
- FusionOrbitMultiplicity.lean 10 declarations
- FusionPacketAction.lean 5 declarations
- FusionPacketLayerExterior.lean 2 declarations
- FusionPacketOrbit.lean 8 declarations
- FusionPacketPerm.lean 9 declarations
- FusionProfilePositiveEvery.lean 3 declarations
- FusionQuiverCartan.lean 1 declarations
- FusionQuiverSimpleEdge.lean 5 declarations
- FusionRest.lean 12 declarations
- FusionSignedPacketExterior.lean 5 declarations
- FusionSubobjectCartanInequality.lean 3 declarations
- FusionVertex.lean 9 declarations
- FusionZeroLabel.lean 4 declarations
- GeneratorPlacement.lean 11 declarations
- GroupProbeEuler.lean 1 declarations
- Harmonic.lean 15 declarations
- HarmonicExtension.lean 19 declarations
- HarmonicUpperAntitone.lean 3 declarations
- Incidence.lean 10 declarations
- IncidentNonnegRowPositive.lean 7 declarations
- Initial.lean 8 declarations
- InitialProbe.lean 5 declarations
- InjectiveFinrankOne.lean 1 declarations
- InsertOldIso.lean 6 declarations
- IntegerUpward.lean 1 declarations
- IntegralQuadratic.lean 5 declarations
- IntegralRowReflect.lean 8 declarations
- IntegralRowReflectApply.lean 3 declarations
- IsolatedBoundaryAbsent.lean 3 declarations
- IsolatedHarmonicLayer.lean 1 declarations
- IsolatedIterationData.lean 12 declarations
- LateDelay.lean 12 declarations
- LayerExpression.lean 8 declarations
- LeftSector.lean 9 declarations
- Level.lean 10 declarations
- LiftedDeck.lean 9 declarations
- LiftedDeckOrderHom.lean 12 declarations
- LiftedPuncturedBoundary.lean 4 declarations
- LowerIneligibleLater.lean 3 declarations
- MapPacket.lean 4 declarations
- MaximalReducedMonoidPrefix.lean 3 declarations
- MaximalReducedPositivePrefix.lean 3 declarations
- MultiplicitySum.lean 3 declarations
- MultiplicityZero.lean 2 declarations
- NegativePrepend.lean 3 declarations
- NeighborhoodProject.lean 3 declarations
- NullPatch.lean 2 declarations
- NullPatch2.lean 10 declarations
- OrderMappingCylinder.lean 17 declarations
- PacketWord.lean 5 declarations
- PeakSupport.lean 16 declarations
- PlacementLevelFiberSum.lean 2 declarations
- PositiveComponent.lean 13 declarations
- PositiveComponentPositive.lean 6 declarations
- PositiveDegreeHom.lean 19 declarations
- PositiveDegreeSublevelFinite.lean 4 declarations
- PositiveDescentSet.lean 5 declarations
- PositiveEarlierLinkUpper.lean 8 declarations
- PositiveGradientStep.lean 3 declarations
- PositiveHead.lean 4 declarations
- PositiveLiftSimple.lean 9 declarations
- PositiveMatchingTypeKey.lean 5 declarations
- PositivePrefix.lean 12 declarations
- PositivePrefixMulLeft.lean 7 declarations
- PositiveRegion.lean 5 declarations
- PositiveRegionDeckIso.lean 6 declarations
- PositiveReverseHom.lean 12 declarations
- PositiveSimpleLiftMul.lean 8 declarations
- PositiveSupportComponent.lean 15 declarations
- PositiveUpperBoundaryRank.lean 3 declarations
- PositiveUpperBoundaryRestriction.lean 4 declarations
- PositiveWord.lean 9 declarations
- PredAboveSuccSucc.lean 9 declarations
- PrincipalOrderIso.lean 17 declarations
- PrismFlag.lean 16 declarations
- PrismGrid.lean 7 declarations
- PrismPrefix.lean 16 declarations
- PrismSimplexZero.lean 7 declarations
- ProbeActionEmbeddedHom.lean 3 declarations
- ProbeActionLevelExterior.lean 5 declarations
- ProbeActionTotalHom.lean 1 declarations
- ProbeCoreInclusion.lean 9 declarations
- ProbeCoreTermNonpos.lean 3 declarations
- ProbeFixedDiagonal.lean 2 declarations
- ProbeFixedOutside.lean 5 declarations
- ProbeOrbitAbsent.lean 4 declarations
- ProbePacket.lean 7 declarations
- ProbePacketExterior.lean 4 declarations
- ProbePositiveWord.lean 10 declarations
- ProbePositiveWordAppend.lean 4 declarations
- ProbePositiveWordInitial.lean 5 declarations
- ProbePositiveWordLeft.lean 3 declarations
- ProbePositiveWordMonoid.lean 4 declarations
- ProbePositiveWordPositive.lean 2 declarations
- ProbeRaiseLower.lean 2 declarations
- ProductBoxSlice.lean 9 declarations
- PuncturedBoundaryIso.lean 6 declarations
- QuantumNumber.lean 17 declarations
- ReducedExpression.lean 13 declarations
- ResidueActive.lean 16 declarations
- ResidueActiveEmpty.lean 3 declarations
- ResidueAllowed.lean 11 declarations
- ResidueEarlierLower.lean 15 declarations
- ResidueEarlierLowerIso.lean 7 declarations
- ResidueHeightZeroVector.lean 5 declarations
- ResidueRank.lean 15 declarations
- ResidueSingleOpen.lean 1 declarations
- ResidueZeroLowerIso.lean 4 declarations
- RestrictedArtinHom.lean 6 declarations
- RestrictedArtinHomSpherical.lean 1 declarations
- RestrictionHomRange.lean 4 declarations
- RootExtension.lean 15 declarations
- RootInclusionRange.lean 3 declarations
- RowReflect.lean 8 declarations
- RowReflectWordReverse.lean 9 declarations
- SecondaryAsSum.lean 7 declarations
- SignedLetter.lean 8 declarations
- SimpleFrontLink.lean 8 declarations
- SimplexSupport.lean 10 declarations
- SpecialResidueRank.lean 2 declarations
- SphericalFoldedMatrix.lean 5 declarations
- SphericalLongest.lean 14 declarations
- SphericalPacketWordProperty.lean 1 declarations
- SphericalPair.lean 1 declarations
- SphericalPositiveCommonMultiple.lean 2 declarations
- SphericalTypeReindex.lean 9 declarations
- Stage.lean 2 declarations
- StringAdjacent.lean 11 declarations
- SumNeighborsSubtype.lean 3 declarations
- SwitchIndex.lean 6 declarations
- TieCode.lean 11 declarations
- TopBlockMatchingKey.lean 9 declarations
- TypeComponent.lean 14 declarations
- TypedRightCoset.lean 7 declarations
- UnfoldedColorOrthogonal.lean 4 declarations
- UnfoldedFullWordMem.lean 4 declarations
- UnfoldedHom.lean 12 declarations
- UnfoldedInclusion.lean 7 declarations
- UnfoldedInclusionRange.lean 6 declarations
- UnfoldedInclusionRangeMono.lean 4 declarations
- UnfoldedMatrix.lean 10 declarations
- UnionCarrier.lean 13 declarations
- WordArtinSubtypeMem.lean 2 declarations
- WordFrontData.lean 8 declarations