OAI/NumberTheory/PiExponent/Geometry/ProjectiveLineCharts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PiExponent.ProjectiveLine.boolChartVariablesUnique line 15
2. def OAI.PiExponent.ProjectiveLine.lineEvaluation line 22
3. theorem OAI.PiExponent.ProjectiveLine.lineEvaluation_X line 25
4. theorem OAI.PiExponent.ProjectiveLine.lineEvaluation_C line 29
5. def OAI.PiExponent.ProjectiveLine.chartRingEquiv line 33
6. lemma OAI.PiExponent.ProjectiveLine.unique_dehomogenize line 37
7. lemma OAI.PiExponent.ProjectiveLine.chartRingEquiv_eq_evalAway line 49
8. def OAI.PiExponent.ProjectiveLine.chartMap line 66
9. instance OAI.PiExponent.ProjectiveLine.chartRingEquiv_isIso line 70
10. instance OAI.PiExponent.ProjectiveLine.chartMap_isOpenImmersion line 74
11. lemma OAI.PiExponent.ProjectiveLine.chartMap_eq_fromUnitCoordinate line 78
12. lemma OAI.PiExponent.ProjectiveLine.chartMap_opensRange line 84
13. lemma OAI.PiExponent.ProjectiveLine.chartMap_cover line 89
14. lemma OAI.PiExponent.ProjectiveLine.chartMap_preimage line 93
15. lemma OAI.PiExponent.ProjectiveLine.chartMap_preimage_other line 99
16. lemma OAI.PiExponent.ProjectiveLine.chartMap_structureMap line 105