OAI/NumberTheory/PiExponent/Geometry/CurveValuationCenter.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveValuationCenter.integral_mem_valuationSubring line 12
  2. theorem OAI.PiExponent.CurveValuationCenter.aeval_mem_valuationSubring line 28
  3. theorem OAI.PiExponent.CurveValuationCenter.parameterChart_mem_valuationSubring line 42
  4. def OAI.PiExponent.CurveValuationCenter.parameterChartValuationHom line 54
  5. def OAI.PiExponent.CurveValuationCenter.parameterValuationCenter line 65
  6. instance OAI.PiExponent.CurveValuationCenter.parameterValuationCenter_isPrime line 73
  7. theorem OAI.PiExponent.CurveValuationCenter.mem_parameterValuationCenter_iff line 80
  8. theorem OAI.PiExponent.CurveValuationCenter.parameterValuationCenter_liesOver line 90
  9. def OAI.PiExponent.CurveValuationCenter.parameterCenterPlace line 107
  10. def OAI.PiExponent.CurveValuationCenter.parameterCenterLocalHom line 116
  11. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterLocalHom_algebraMap line 129
  12. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterLocalHom_comap_maximalIdeal line 138
  13. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterLocalHom_coe line 155
  14. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterLocal_nonneg line 175
  15. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterLocal_positive line 188
  16. theorem OAI.PiExponent.CurveValuationCenter.primeFieldValuation_algebraMap_localOrder line 205
  17. theorem OAI.PiExponent.CurveValuationCenter.primeFieldValuation_algebraMap_nonneg line 226
  18. theorem OAI.PiExponent.CurveValuationCenter.enatToIntegerOrder_pos_iff line 234
  19. theorem OAI.PiExponent.CurveValuationCenter.primeFieldValuation_positive_iff line 242
  20. structure OAI.PiExponent.CurveValuationCenter.NormalizedPlace line 254
  21. theorem OAI.PiExponent.CurveValuationCenter.NormalizedPlace.ext line 259
  22. theorem OAI.PiExponent.CurveValuationCenter.valuation_eq_parameterPlaceValuation line 267
  23. theorem OAI.PiExponent.CurveValuationCenter.primeFieldValuation_normalized line 300
  24. theorem OAI.PiExponent.CurveValuationCenter.parameterPlaceValuation_constants_nonneg line 314
  25. theorem OAI.PiExponent.CurveValuationCenter.parameterPlaceValuation_positive line 335
  26. def OAI.PiExponent.CurveValuationCenter.parameterNormalizedPlace line 360
  27. theorem OAI.PiExponent.CurveValuationCenter.parameterCenterPlace_parameterNormalizedPlace line 378
  28. def OAI.PiExponent.CurveValuationCenter.positivePlaceEquivZeroPlaces line 402
  29. theorem OAI.PiExponent.CurveValuationCenter.finite_positivePlaces line 416