OAI/RepresentationTheory/RestrictedTilting/BoundedOriginTarget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FiberFunctorProof.EquivariantPlaneBundle line 13
2. def OAI.FiberFunctorProof.planePointIdeal line 32
3. def OAI.FiberFunctorProof.EquivariantPlaneBundle.fibreRelation line 35
4. abbrev OAI.FiberFunctorProof.EquivariantPlaneBundle.fibre line 39
5. def OAI.FiberFunctorProof.HasHighestWeight line 44
6. def OAI.FiberFunctorProof.AllSimpleFactorsHighestBelow line 52
7. def OAI.FiberFunctorProof.BoundedOriginTheorem line 62