OAI/NumberTheory/PiExponent/Geometry/AdmissibleCurveCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.AdmissibleCurveCoordinates.imageCurve line 15
  2. abbrev OAI.PiExponent.AdmissibleCurveCoordinates.sourceStructure line 16
  3. abbrev OAI.PiExponent.AdmissibleCurveCoordinates.imageStructure line 17
  4. def OAI.PiExponent.AdmissibleCurveCoordinates.sourceAlgebra line 18
  5. def OAI.PiExponent.AdmissibleCurveCoordinates.imageAlgebra line 20
  6. def OAI.PiExponent.AdmissibleCurveCoordinates.fieldEquiv line 24
  7. abbrev OAI.PiExponent.AdmissibleCurveCoordinates.chart line 34
  8. abbrev OAI.PiExponent.AdmissibleCurveCoordinates.chartPresentation line 35
  9. theorem OAI.PiExponent.AdmissibleCurveCoordinates.chart_nonempty line 40
  10. def OAI.PiExponent.AdmissibleCurveCoordinates.imageCoordinates line 43
  11. def OAI.PiExponent.AdmissibleCurveCoordinates.coordinates line 47
  12. def OAI.PiExponent.AdmissibleCurveCoordinates.y line 52
  13. def OAI.PiExponent.AdmissibleCurveCoordinates.x line 54
  14. theorem OAI.PiExponent.AdmissibleCurveCoordinates.full_coordinates line 56
  15. theorem OAI.PiExponent.AdmissibleCurveCoordinates.field_properties line 62
  16. theorem OAI.PiExponent.AdmissibleCurveCoordinates.coordinates_generic_map line 78