OAI/NumberTheory/PiExponent/Geometry/CurveModelPlaces.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveModelPlaces.parameterValuationCenter_ne_bot line 16
  2. def OAI.PiExponent.CurveModelPlaces.chartCenter line 49
  3. def OAI.PiExponent.CurveModelPlaces.chartValuation line 59
  4. theorem OAI.PiExponent.CurveModelPlaces.valuation_eq_chartCenter line 74
  5. theorem OAI.PiExponent.CurveModelPlaces.chartValuation_nonneg line 101
  6. theorem OAI.PiExponent.CurveModelPlaces.chartValuation_positive_iff line 113
  7. def OAI.PiExponent.CurveModelPlaces.chartPlace line 125
  8. theorem OAI.PiExponent.CurveModelPlaces.chartPlace_parameter_nonneg line 147
  9. theorem OAI.PiExponent.CurveModelPlaces.chartPlace_chartCenter line 161
  10. theorem OAI.PiExponent.CurveModelPlaces.chartCenter_chartPlace line 169
  11. def OAI.PiExponent.CurveModelPlaces.regularPlacesEquivChartPrimes line 181
  12. theorem OAI.PiExponent.CurveModelPlaces.parameterLaurentMap_mem line 192
  13. theorem OAI.PiExponent.CurveModelPlaces.parameterLaurentChart_mem line 215
  14. def OAI.PiExponent.CurveModelPlaces.laurentValuationHom line 225
  15. def OAI.PiExponent.CurveModelPlaces.laurentCenter line 236
  16. theorem OAI.PiExponent.CurveModelPlaces.laurentCenter_zero line 244
  17. theorem OAI.PiExponent.CurveModelPlaces.laurentCenter_infinity line 254
  18. theorem OAI.PiExponent.CurveModelPlaces.center_images_eq line 265
  19. theorem OAI.PiExponent.CurveModelPlaces.regular_iff_inverse_not_positive line 278
  20. theorem OAI.PiExponent.CurveModelPlaces.inverse_positive_of_not_regular line 290
  21. def OAI.PiExponent.CurveModelPlaces.placePoint line 296
  22. theorem OAI.PiExponent.CurveModelPlaces.placePoint_eq_zero line 308
  23. theorem OAI.PiExponent.CurveModelPlaces.placePoint_eq_infinity line 316
  24. theorem OAI.PiExponent.CurveModelPlaces.placePoint_ne_genericPoint line 328
  25. theorem OAI.PiExponent.CurveModelPlaces.regular_center_injective line 351
  26. theorem OAI.PiExponent.CurveModelPlaces.placePoint_mem_zero_iff line 365
  27. theorem OAI.PiExponent.CurveModelPlaces.placePoint_injective line 396
  28. theorem OAI.PiExponent.CurveModelPlaces.exists_placePoint_eq line 419
  29. def OAI.PiExponent.CurveModelPlaces.placesEquivNongenericPoints line 465
  30. def OAI.PiExponent.CurveModelPlaces.placesEquivClosedPoints line 476