OAI/NumberTheory/PiExponent/Geometry/CurveZeroPole.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CurveZeroPole.fiberDegree line 11
  2. theorem OAI.PiExponent.CurveZeroPole.fiberDegree_eq_rank line 16
  3. theorem OAI.PiExponent.CurveZeroPole.fiberDegree_eq_fractionField_rank line 24
  4. theorem OAI.PiExponent.CurveZeroPole.functionField_fiberDegree line 35
  5. theorem OAI.PiExponent.CurveZeroPole.adjoin_inverse_eq line 49
  6. theorem OAI.PiExponent.CurveZeroPole.parameter_inverse_degree_eq line 59
  7. def OAI.PiExponent.CurveZeroPole.parameterEmbedding line 65
  8. theorem OAI.PiExponent.CurveZeroPole.parameterEmbedding_X line 70
  9. abbrev OAI.PiExponent.CurveZeroPole.parameterAlgebra line 74
  10. theorem OAI.PiExponent.CurveZeroPole.parameter_finrank line 78
  11. theorem OAI.PiExponent.CurveZeroPole.parameter_finite line 87
  12. abbrev OAI.PiExponent.CurveZeroPole.parameterPolynomialAlgebra line 100
  13. theorem OAI.PiExponent.CurveZeroPole.parameter_scalarTower line 104
  14. def OAI.PiExponent.CurveZeroPole.zeroPrime line 115
  15. instance OAI.PiExponent.CurveZeroPole.zeroPrime_isPrime line 118
  16. theorem OAI.PiExponent.CurveZeroPole.zeroPrime_eq_span_X line 121
  17. def OAI.PiExponent.CurveZeroPole.parameterFiberDegree line 124
  18. theorem OAI.PiExponent.CurveZeroPole.parameterFiberDegree_eq line 133
  19. theorem OAI.PiExponent.CurveZeroPole.transcendental_inverse line 145
  20. theorem OAI.PiExponent.CurveZeroPole.zero_infinity_fiberDegree_eq line 149
  21. theorem OAI.PiExponent.CurveZeroPole.constantCoeff_surjective line 160
  22. instance OAI.PiExponent.CurveZeroPole.zeroPrime_isMaximal line 165
  23. def OAI.PiExponent.CurveZeroPole.zeroPrimeQuotientEquiv line 168
  24. theorem OAI.PiExponent.CurveZeroPole.zeroFiber_inertiaDeg_eq_one line 171
  25. def OAI.PiExponent.CurveZeroPole.zeroFiberLength line 184
  26. theorem OAI.PiExponent.CurveZeroPole.zeroFiberLength_eq_fiberDegree line 192
  27. def OAI.PiExponent.CurveZeroPole.parameterZeroLength line 210
  28. theorem OAI.PiExponent.CurveZeroPole.parameterZeroLength_eq_degree line 219
  29. theorem OAI.PiExponent.CurveZeroPole.zero_pole_length_eq line 232
  30. def OAI.PiExponent.CurveZeroPole.primeFieldValuation line 243
  31. theorem OAI.PiExponent.CurveZeroPole.primeFieldValuation_algebraMap line 255
  32. theorem OAI.PiExponent.CurveZeroPole.primeField_integerOrder_algebraMap line 277
  33. theorem OAI.PiExponent.CurveZeroPole.zeroPrime_ne_bot line 302
  34. def OAI.PiExponent.CurveZeroPole.zeroFiberHeightOne line 310
  35. theorem OAI.PiExponent.CurveZeroPole.baseParameter_nonzero line 315
  36. def OAI.PiExponent.CurveZeroPole.zeroFiberIntegerOrderSum line 323
  37. theorem OAI.PiExponent.CurveZeroPole.zeroFiberIntegerOrderSum_eq_length line 332
  38. def OAI.PiExponent.CurveZeroPole.parameterZeroOrder line 362
  39. theorem OAI.PiExponent.CurveZeroPole.parameterZeroOrder_eq_length line 374
  40. theorem OAI.PiExponent.CurveZeroPole.zero_pole_order_eq line 388
  41. abbrev OAI.PiExponent.CurveZeroPole.parameterChart line 399
  42. abbrev OAI.PiExponent.CurveZeroPole.parameterZeroPlaces line 404
  43. abbrev OAI.PiExponent.CurveZeroPole.parameterZeroPlacesFintype line 409
  44. def OAI.PiExponent.CurveZeroPole.parameterPlaceValuation line 421
  45. theorem OAI.PiExponent.CurveZeroPole.parameterPolynomialAlgebra_map line 436
  46. theorem OAI.PiExponent.CurveZeroPole.parameterZeroOrder_eq_sum line 447
  47. theorem OAI.PiExponent.CurveZeroPole.sum_zero_and_pole_orders_eq_zero line 471