OAI/GroupTheory/FiniteType/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 135 imports below, so a file that imports it gets all of them.
Imports
- OAI.GroupTheory.FiniteType.PresentationGeometry
- OAI.GroupTheory.FiniteType.PresentationVanKampen
- OAI.GroupTheory.FiniteType.PresentationGeometryDescend
- OAI.GroupTheory.FiniteType.PresentationGeometryCells
- OAI.GroupTheory.FiniteType.SphereCover
- OAI.GroupTheory.FiniteType.RegularCoverGeometry
- OAI.GroupTheory.FiniteType.FiberCoreMap
- OAI.GroupTheory.FiniteType.PresentationGeometryCellCoverExtension
- OAI.GroupTheory.FiniteType.AffineSimplex
- OAI.GroupTheory.FiniteType.SingularSubdivision
- OAI.GroupTheory.FiniteType.SingularSupport
- OAI.GroupTheory.FiniteType.SingularSubdivisionIterate
- OAI.GroupTheory.FiniteType.SingularSubdivisionIterateApplyComm
- OAI.GroupTheory.FiniteType.QuotientComplex
- OAI.GroupTheory.FiniteType.SingularExcision
- OAI.GroupTheory.FiniteType.RelativeChains
- OAI.GroupTheory.FiniteType.DiskRadial
- OAI.GroupTheory.FiniteType.DiskSigmaCollar
- OAI.GroupTheory.FiniteType.ChainShortExact
- OAI.GroupTheory.FiniteType.RelativeChainsEmptyProjectionQuasiIso
- OAI.GroupTheory.FiniteType.SingularSigma
- OAI.GroupTheory.FiniteType.CWCellular
- OAI.GroupTheory.FiniteType.CWCellularSkelInclHomologyIsIso
- OAI.GroupTheory.FiniteType.CoveringCellGeometry
- OAI.GroupTheory.FiniteType.CoveringCellGeometryHausdorff
- OAI.GroupTheory.FiniteType.PresentationGeometryCellCoverExtensionAnyAttachingLiftNullhomotopic
- OAI.GroupTheory.FiniteType.DiskHEP
- OAI.GroupTheory.FiniteType.CWCylinder
- OAI.GroupTheory.FiniteType.SphereQuotient
- OAI.GroupTheory.FiniteType.CubeDisk
- OAI.GroupTheory.FiniteType.SimplexHomotopy
- OAI.GroupTheory.FiniteType.SingularPrism
- OAI.GroupTheory.FiniteType.HomotopyFunctor
- OAI.GroupTheory.FiniteType.SingularSphereCycle
- OAI.GroupTheory.FiniteType.DuffySimplex
- OAI.GroupTheory.FiniteType.DuffyTriangle
- OAI.GroupTheory.FiniteType.LoopPath
- OAI.GroupTheory.FiniteType.BasedHorn
- OAI.GroupTheory.FiniteType.SimplexRotation
- OAI.GroupTheory.FiniteType.SimplexSign
- OAI.GroupTheory.FiniteType.BoundaryValue
- OAI.GroupTheory.FiniteType.HornElimination
- OAI.GroupTheory.FiniteType.BoundaryValueBoundarySplit
- OAI.GroupTheory.FiniteType.HurewiczInverse
- OAI.GroupTheory.FiniteType.RepresentationKilling
- OAI.GroupTheory.FiniteType.SingularSigmaSingleMerge
- OAI.GroupTheory.FiniteType.SingularChains
- OAI.GroupTheory.FiniteType.ProductFiniteResolution
- OAI.GroupTheory.FiniteType.PartialResolution
- OAI.GroupTheory.FiniteType.PartialResolutionPartialCyclesFg
- OAI.GroupTheory.FiniteType.SingularAction
- OAI.GroupTheory.FiniteType.CoreDeck
- OAI.GroupTheory.FiniteType.PresentationVanKampenRectanglePaths
- OAI.GroupTheory.FiniteType.PresentationGeometryRose
- OAI.GroupTheory.FiniteType.CoreDeckLeftQuotientCovering
- OAI.GroupTheory.FiniteType.SequentialColimit
- OAI.GroupTheory.FiniteType.SequentialColimitRangeInclMono
- OAI.GroupTheory.FiniteType.CWWhitehead
- OAI.GroupTheory.FiniteType.PresentationGeometryFiniteStage
- OAI.GroupTheory.FiniteType.FreeTensor
- OAI.GroupTheory.FiniteType.BasedComplex
- OAI.GroupTheory.FiniteType.FreeTensorPureMem
- OAI.GroupTheory.FiniteType.ListChains
- OAI.GroupTheory.FiniteType.ListChainsHasPropagation
- OAI.GroupTheory.FiniteType.ListChainsMapChainComp
- OAI.GroupTheory.FiniteType.FiniteIdempotentDiagrams
- OAI.GroupTheory.FiniteType.BinaryPrefixOperators
- OAI.GroupTheory.FiniteType.ListChainsShiftOrigin
- OAI.GroupTheory.FiniteType.UniformProductSupport
- OAI.GroupTheory.FiniteType.ProductCoefficient
- OAI.GroupTheory.FiniteType.Representation
- OAI.GroupTheory.FiniteType.ListChainsFromTuplesCone
- OAI.GroupTheory.FiniteType.ProductCoefficientAffineShift
- OAI.GroupTheory.FiniteType.StandardShapiro
- OAI.GroupTheory.FiniteType.CosetInduction
- OAI.GroupTheory.FiniteType.SemilinearCoinvariants
- OAI.GroupTheory.FiniteType.CosetCoordinates
- OAI.GroupTheory.FiniteType.CategoryTheoryShortComplex
- OAI.GroupTheory.FiniteType.StandardHomology
- OAI.GroupTheory.FiniteType.AscendingHNN
- OAI.GroupTheory.FiniteType.AscendingTorus
- OAI.GroupTheory.FiniteType.ClassifyingSpaces
- OAI.GroupTheory.FiniteType.FiniteIndexRegular
- OAI.GroupTheory.FiniteType.ClassifyingSpacesFiniteExtensionGeometricFromProducts
- OAI.GroupTheory.FiniteType.Steinberg
- OAI.GroupTheory.FiniteType.NonunitalCompression
- OAI.GroupTheory.FiniteType.RingExchange
- OAI.GroupTheory.FiniteType.CompressedSplittings
- OAI.GroupTheory.FiniteType.SteinbergSixThree
- OAI.GroupTheory.FiniteType.PrefixPermutation
- OAI.GroupTheory.FiniteType.StageConstruction
- OAI.GroupTheory.FiniteType.SequentialLimit
- OAI.GroupTheory.FiniteType.TorusAction
- OAI.GroupTheory.FiniteType.SteinbergWords
- OAI.GroupTheory.FiniteType.SteinbergFinitePresentation
- OAI.GroupTheory.FiniteType.AscendingHNNInnerTwist
- OAI.GroupTheory.FiniteType.HomStabilizer
- OAI.GroupTheory.FiniteType.BinaryAlgebraPresentation
- OAI.GroupTheory.FiniteType.SourceCorner
- OAI.GroupTheory.FiniteType.ProductCriterion
- OAI.GroupTheory.FiniteType.InducedFree
- OAI.GroupTheory.FiniteType.ProductFiniteResolutionBeginningOfComplex
- OAI.GroupTheory.FiniteType.SurjectiveTrivialInduction
- OAI.GroupTheory.FiniteType.ProductGroupHomology
- OAI.GroupTheory.FiniteType.TwistedBrin
- OAI.GroupTheory.FiniteType.TwistedBrinRangeChartRestricts
- OAI.GroupTheory.FiniteType.TwistedBrinBasis
- OAI.GroupTheory.FiniteType.TwistedBrinPrefix
- OAI.GroupTheory.FiniteType.TwistedBrinBasisTranslateEquiv
- OAI.GroupTheory.FiniteType.TwistedBrinPattern
- OAI.GroupTheory.FiniteType.TwistedBrinGermBrick
- OAI.GroupTheory.FiniteType.TwistedBrinPatternFactor
- OAI.GroupTheory.FiniteType.TwistedBrinBasisFirstCut
- OAI.GroupTheory.FiniteType.OrderListChains
- OAI.GroupTheory.FiniteType.OrderBasedComplex
- OAI.GroupTheory.FiniteType.OrderListChainsBased
- OAI.GroupTheory.FiniteType.OrderChains
- OAI.GroupTheory.FiniteType.OrderChainsExactInOfTop
- OAI.GroupTheory.FiniteType.OrderChainsOnSet
- OAI.GroupTheory.FiniteType.OrderListChainsVertexSupport
- OAI.GroupTheory.FiniteType.OrderChainsExactInOfDirected
- OAI.GroupTheory.FiniteType.TwistedBrinBasisGroundMatching
- OAI.GroupTheory.FiniteType.PosetTransport
- OAI.GroupTheory.FiniteType.TwistedBrinBasisMatching
- OAI.GroupTheory.FiniteType.ActionTransport
- OAI.GroupTheory.FiniteType.TwistedBrinBasisCutBasis
- OAI.GroupTheory.FiniteType.EquivariantOrderChains
- OAI.GroupTheory.FiniteType.FiniteIndexProducts
- OAI.GroupTheory.FiniteType.OrderChainsExactSubtypeOfExactSet
- OAI.GroupTheory.FiniteType.TwistedBrinEquiv
- OAI.GroupTheory.FiniteType.TwistedBrinSeparated
- OAI.GroupTheory.FiniteType.StageGeometry
- OAI.GroupTheory.FiniteType.StageGeometryProperties
- OAI.GroupTheory.FiniteType.IdempotentEnlargement
- OAI.GroupTheory.FiniteType.SourceEnlargement