OAI/CategoryTheory/ThickClosure/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 30 imports below, so a file that imports it gets all of them.
Imports
- OAI.CategoryTheory.ThickClosure.PrincipalModules
- OAI.CategoryTheory.ThickClosure.PeriodicSplitting
- OAI.CategoryTheory.ThickClosure.PeriodicDerived
- OAI.CategoryTheory.ThickClosure.PeriodicHom
- OAI.CategoryTheory.ThickClosure.LocalizationHom
- OAI.CategoryTheory.ThickClosure.DerivedHom
- OAI.CategoryTheory.ThickClosure.CyclicStructure
- OAI.CategoryTheory.ThickClosure.Unroll
- OAI.CategoryTheory.ThickClosure.CyclicShift
- OAI.CategoryTheory.ThickClosure.UnrollDerived
- OAI.CategoryTheory.ThickClosure.CyclicTriangle
- OAI.CategoryTheory.ThickClosure.PeriodicDual
- OAI.CategoryTheory.ThickClosure.GradedSplit
- OAI.CategoryTheory.ThickClosure.HomologyBridge
- OAI.CategoryTheory.ThickClosure.FiniteTower
- OAI.CategoryTheory.ThickClosure.FreeHomology
- OAI.CategoryTheory.ThickClosure.BackwardStep
- OAI.CategoryTheory.ThickClosure.PeriodicBackward
- OAI.CategoryTheory.ThickClosure.Criterion
- OAI.CategoryTheory.ThickClosure.LaurentModules
- OAI.CategoryTheory.ThickClosure.LaurentCriterion
- OAI.CategoryTheory.ThickClosure.PerfectModules
- OAI.CategoryTheory.ThickClosure.SourceCriterion
- OAI.CategoryTheory.ThickClosure.LaurentAction
- OAI.CategoryTheory.ThickClosure.ActionDerived
- OAI.CategoryTheory.ThickClosure.Coefficients
- OAI.LinearAlgebra.RankMatching.Basic
- OAI.Topology.HahnSeries.Pivots
- OAI.RingTheory.Interpolation.Bounds
- OAI.CategoryTheory.ThickClosure.FiniteProducts