OAI/RepresentationTheory/RestrictedTilting/XChartLineEval.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.planeLineEval line 9
2. lemma OAI.FiberFunctorProof.planeLineEval_X_isUnit line 12
3. def OAI.FiberFunctorProof.chartLineEval line 16
4. lemma OAI.FiberFunctorProof.chartLineEval_algebraMap line 19
5. lemma OAI.FiberFunctorProof.chartLineEval_coordinate line 23
6. lemma OAI.FiberFunctorProof.chartLineEval_inverse line 28
7. lemma OAI.FiberFunctorProof.planeXPolynomialChart_line line 36
8. lemma OAI.FiberFunctorProof.regularXChartValue_line line 49
9. lemma OAI.FiberFunctorProof.associatedXChart_line line 59
10. lemma OAI.FiberFunctorProof.unipotent_inverse line 66
11. lemma OAI.FiberFunctorProof.associatedSections_line_unipotent line 71