OAI/RepresentationTheory/RestrictedTilting/FormalAssociatedIso.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiberFunctorProof.ofPowerSeriesAlg_apply_eq line 32
2. def OAI.FiberFunctorProof.formalLineParameter line 35
3. lemma OAI.FiberFunctorProof.formalLineParameter_ne_zero line 39
4. def OAI.FiberFunctorProof.associatedFieldTrivialization line 44
5. lemma OAI.FiberFunctorProof.associatedFieldTrivialization_one line 58
6. lemma OAI.FiberFunctorProof.associatedFieldTrivialization_unipotent_one line 70