OAI/NumberTheory/PiExponent/Geometry/ProjectiveLineProper.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.ProjectiveLine.projectiveLine line 13
2. def OAI.PiExponent.ProjectiveLine.constantsInDegreeZero line 16
3. theorem OAI.PiExponent.ProjectiveLine.constantsInDegreeZero_bijective line 24
4. def OAI.PiExponent.ProjectiveLine.degreeZeroEquiv line 36
5. instance OAI.PiExponent.ProjectiveLine.constantsInDegreeZero_isIso line 40
6. def OAI.PiExponent.ProjectiveLine.structureMap line 44
7. instance OAI.PiExponent.ProjectiveLine.structureMap_isProper line 49