OAI/RepresentationTheory/RestrictedTilting/AssociatedFibre.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.associatedE1Equiv line 19
2. lemma OAI.FiberFunctorProof.planeLineEval_one line 28
3. lemma OAI.FiberFunctorProof.associatedNumerator_e1 line 34
4. lemma OAI.FiberFunctorProof.associatedE1Equiv_mk line 46
5. lemma OAI.FiberFunctorProof.associatedE1Equiv_unipotent line 52