OAI/RepresentationTheory/RestrictedTilting/TiltingCovers.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- inductive
OAI.FiberFunctorProof.SteinbergGeneratedline 13 - lemma
OAI.FiberFunctorProof.SteinbergGenerated.tiltingline 23 - lemma
OAI.FiberFunctorProof.costandard_generated_coverline 33 - lemma
OAI.FiberFunctorProof.good_generated_coverline 62 - theorem
OAI.FiberFunctorProof.tilting_retract_generatedline 88