OAI/RepresentationTheory/RestrictedTilting/StableRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiberFunctorProof.Tilting line 13
2. abbrev OAI.FiberFunctorProof.tiltingInclusion line 16
3. def OAI.FiberFunctorProof.steinbergIdeal line 21
4. theorem OAI.FiberFunctorProof.restricted_steinberg_projective line 32
5. theorem OAI.FiberFunctorProof.steinbergIdeal_restricts_projectively line 39