OAI/RingTheory/Kurosh/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 19 imports below, so a file that imports it gets all of them.
Imports
- OAI.RingTheory.Kurosh.FreeSeries
- OAI.RingTheory.Kurosh.SeriesAlgebra
- OAI.RingTheory.Kurosh.Lifting
- OAI.RingTheory.Kurosh.ScalarChange
- OAI.RingTheory.Kurosh.LiftingStages
- OAI.RingTheory.Kurosh.TangentDirections
- OAI.RingTheory.Kurosh.ScheduledTowers
- OAI.RingTheory.Kurosh.RetainedRelations
- OAI.RingTheory.Kurosh.Ultraproduct
- OAI.RingTheory.Kurosh.LimitScalars
- OAI.RingTheory.Kurosh.LimitEvaluation
- OAI.RingTheory.Kurosh.Independence
- OAI.RingTheory.Kurosh.WordGrowth
- OAI.RingTheory.Kurosh.IndependentWords
- OAI.RingTheory.Kurosh.InfiniteDimension
- OAI.RingTheory.Kurosh.AlgebraicClosure
- OAI.RingTheory.Kurosh.FiniteDescent
- OAI.RingTheory.Kurosh.ScheduledLimit
- OAI.RingTheory.Kurosh.ConditionalConstruction