OAI/RepresentationTheory/RestrictedTilting/FormalSections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.adicPlaneSections line 19
2. lemma OAI.FiberFunctorProof.adicPlaneSections_succ line 25
3. lemma OAI.FiberFunctorProof.adicPlaneSections_transition line 47
4. lemma OAI.FiberFunctorProof.adicPlaneSections_origin line 58
5. lemma OAI.FiberFunctorProof.adicPlaneSections_bijective line 65
6. def OAI.FiberFunctorProof.formalPlaneSection line 99
7. lemma OAI.FiberFunctorProof.formalPlaneSection_equivariant line 110
8. def OAI.FiberFunctorProof.formalPlaneTrivialization line 122
9. lemma OAI.FiberFunctorProof.formalPlaneTrivialization_one_tmul line 138
10. theorem OAI.FiberFunctorProof.exists_formalPlaneTrivialization line 158