OAI/NumberTheory/PiExponent/Geometry/CurveGeometricFunctionField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveGeometricFunctionField.fractionField_essFiniteType line 18
  2. theorem OAI.PiExponent.CurveGeometricFunctionField.fractionField_trdeg_eq_one line 24
  3. def OAI.PiExponent.CurveGeometricFunctionField.coordinates line 35
  4. theorem OAI.PiExponent.CurveGeometricFunctionField.adjoin_coordinates_eq_top line 39
  5. theorem OAI.PiExponent.CurveGeometricFunctionField.of_surjective_coordinates line 59
  6. theorem OAI.PiExponent.CurveGeometricFunctionField.finite_over_every_parameter line 68
  7. theorem OAI.PiExponent.CurveGeometricFunctionField.ringKrullDim_eq_one_of_affine_iso line 77
  8. theorem OAI.PiExponent.CurveGeometricFunctionField.of_affine_curve line 85
  9. def OAI.PiExponent.CurveGeometricFunctionField.intrinsicSectionAlgebra line 93
  10. def OAI.PiExponent.CurveGeometricFunctionField.intrinsicFunctionFieldAlgebra line 100
  11. theorem OAI.PiExponent.CurveGeometricFunctionField.intrinsic_functionField line 105