OAI/RepresentationTheory/RestrictedTilting/Basic.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 4 imports below, so a file that imports it gets all of them.
Imports
Imported by 10 files
- OAI/RepresentationTheory/RestrictedTilting/BoundedOriginTarget.lean
- OAI/RepresentationTheory/RestrictedTilting/BoundedStableFaithfulness.lean
- OAI/RepresentationTheory/RestrictedTilting/CompatibleJets.lean
- OAI/RepresentationTheory/RestrictedTilting/LatticeNumerator.lean
- OAI/RepresentationTheory/RestrictedTilting/Main.lean
- OAI/RepresentationTheory/RestrictedTilting/RationalHomWeights.lean
- OAI/RepresentationTheory/RestrictedTilting/RationalMatrices.lean
- OAI/RepresentationTheory/RestrictedTilting/SteinbergRegular.lean
- OAI/RepresentationTheory/RestrictedTilting/TorusWeightProjection.lean
- OAI/RepresentationTheory/RestrictedTilting/XChartLineEval.lean