OAI/GroupTheory/FiniteType/
4726 declarations, 0 contain sorry, 0 declared as axioms; 136 files
Files
- ActionTransport.lean 10 declarations
- AffineSimplex.lean 50 declarations
- AscendingHNN.lean 41 declarations
- AscendingHNNInnerTwist.lean 47 declarations
- AscendingTorus.lean 32 declarations
- BasedComplex.lean 21 declarations
- BasedHorn.lean 27 declarations
- BinaryAlgebraPresentation.lean 10 declarations
- BinaryPrefixOperators.lean 61 declarations
- BoundaryValue.lean 21 declarations
- BoundaryValueBoundarySplit.lean 29 declarations
- CWCellular.lean 31 declarations
- CWCellularSkelInclHomologyIsIso.lean 17 declarations
- CWCylinder.lean 30 declarations
- CWWhitehead.lean 17 declarations
- CategoryTheoryShortComplex.lean 20 declarations
- ChainShortExact.lean 20 declarations
- ClassifyingSpaces.lean 50 declarations
- ClassifyingSpacesFiniteExtensionGeometricFromProducts.lean 31 declarations
- CompressedSplittings.lean 29 declarations
- CoreDeck.lean 32 declarations
- CoreDeckLeftQuotientCovering.lean 50 declarations
- CosetCoordinates.lean 26 declarations
- CosetInduction.lean 26 declarations
- CoveringCellGeometry.lean 36 declarations
- CoveringCellGeometryHausdorff.lean 19 declarations
- CubeDisk.lean 26 declarations
- DiskHEP.lean 43 declarations
- DiskRadial.lean 52 declarations
- DiskSigmaCollar.lean 40 declarations
- DuffySimplex.lean 32 declarations
- DuffyTriangle.lean 23 declarations
- EquivariantOrderChains.lean 27 declarations
- FiberCoreMap.lean 39 declarations
- FiniteIdempotentDiagrams.lean 30 declarations
- FiniteIndexProducts.lean 20 declarations
- FiniteIndexRegular.lean 24 declarations
- FreeTensor.lean 43 declarations
- FreeTensorPureMem.lean 44 declarations
- HomStabilizer.lean 14 declarations
- HomotopyFunctor.lean 32 declarations
- HornElimination.lean 29 declarations
- HurewiczInverse.lean 32 declarations
- IdempotentEnlargement.lean 38 declarations
- InducedFree.lean 29 declarations
- ListChains.lean 52 declarations
- ListChainsFromTuplesCone.lean 21 declarations
- ListChainsHasPropagation.lean 48 declarations
- ListChainsMapChainComp.lean 33 declarations
- ListChainsShiftOrigin.lean 46 declarations
- LoopPath.lean 30 declarations
- Main.lean 135 imports, no declarations
- NonunitalCompression.lean 66 declarations
- OrderBasedComplex.lean 21 declarations
- OrderChains.lean 31 declarations
- OrderChainsExactInOfDirected.lean 29 declarations
- OrderChainsExactInOfTop.lean 12 declarations
- OrderChainsExactSubtypeOfExactSet.lean 14 declarations
- OrderChainsOnSet.lean 24 declarations
- OrderListChains.lean 72 declarations
- OrderListChainsBased.lean 60 declarations
- OrderListChainsVertexSupport.lean 13 declarations
- PartialResolution.lean 26 declarations
- PartialResolutionPartialCyclesFg.lean 14 declarations
- PosetTransport.lean 48 declarations
- PrefixPermutation.lean 30 declarations
- PresentationGeometry.lean 134 declarations
- PresentationGeometryCellCoverExtension.lean 36 declarations
- PresentationGeometryCellCoverExtensionAnyAttachingLiftNullhomotopic.lean 24 declarations
- PresentationGeometryCells.lean 31 declarations
- PresentationGeometryDescend.lean 57 declarations
- PresentationGeometryFiniteStage.lean 59 declarations
- PresentationGeometryRose.lean 42 declarations
- PresentationVanKampen.lean 29 declarations
- PresentationVanKampenRectanglePaths.lean 38 declarations
- ProductCoefficient.lean 29 declarations
- ProductCoefficientAffineShift.lean 23 declarations
- ProductCriterion.lean 24 declarations
- ProductFiniteResolution.lean 33 declarations
- ProductFiniteResolutionBeginningOfComplex.lean 11 declarations
- ProductGroupHomology.lean 77 declarations
- QuotientComplex.lean 37 declarations
- RegularCoverGeometry.lean 18 declarations
- RelativeChains.lean 23 declarations
- RelativeChainsEmptyProjectionQuasiIso.lean 33 declarations
- Representation.lean 27 declarations
- RepresentationKilling.lean 31 declarations
- RingExchange.lean 49 declarations
- SemilinearCoinvariants.lean 24 declarations
- SequentialColimit.lean 46 declarations
- SequentialColimitRangeInclMono.lean 33 declarations
- SequentialLimit.lean 44 declarations
- SimplexHomotopy.lean 38 declarations
- SimplexRotation.lean 32 declarations
- SimplexSign.lean 29 declarations
- SingularAction.lean 27 declarations
- SingularChains.lean 42 declarations
- SingularExcision.lean 20 declarations
- SingularPrism.lean 35 declarations
- SingularSigma.lean 40 declarations
- SingularSigmaSingleMerge.lean 24 declarations
- SingularSphereCycle.lean 53 declarations
- SingularSubdivision.lean 34 declarations
- SingularSubdivisionIterate.lean 35 declarations
- SingularSubdivisionIterateApplyComm.lean 30 declarations
- SingularSupport.lean 40 declarations
- SourceCorner.lean 24 declarations
- SourceEnlargement.lean 53 declarations
- SphereCover.lean 31 declarations
- SphereQuotient.lean 26 declarations
- StageConstruction.lean 43 declarations
- StageGeometry.lean 19 declarations
- StageGeometryProperties.lean 1 declarations
- StandardHomology.lean 21 declarations
- StandardShapiro.lean 30 declarations
- Steinberg.lean 36 declarations
- SteinbergFinitePresentation.lean 38 declarations
- SteinbergSixThree.lean 26 declarations
- SteinbergWords.lean 33 declarations
- SurjectiveTrivialInduction.lean 41 declarations
- TorusAction.lean 40 declarations
- TwistedBrin.lean 77 declarations
- TwistedBrinBasis.lean 59 declarations
- TwistedBrinBasisCutBasis.lean 32 declarations
- TwistedBrinBasisFirstCut.lean 53 declarations
- TwistedBrinBasisGroundMatching.lean 46 declarations
- TwistedBrinBasisMatching.lean 44 declarations
- TwistedBrinBasisTranslateEquiv.lean 42 declarations
- TwistedBrinEquiv.lean 60 declarations
- TwistedBrinGermBrick.lean 42 declarations
- TwistedBrinPattern.lean 33 declarations
- TwistedBrinPatternFactor.lean 67 declarations
- TwistedBrinPrefix.lean 42 declarations
- TwistedBrinRangeChartRestricts.lean 48 declarations
- TwistedBrinSeparated.lean 13 declarations
- UniformProductSupport.lean 25 declarations