OAI/AlgebraicGeometry/NumericalDimension/AffineCurves.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Affine Curves.

  1. theorem OAI.NumericalDimensionOne.surface_negativity_of_antinef line 17
  2. theorem OAI.NumericalDimensionOne.ringKrullDim_eq_of_integral_faithful line 112
  3. theorem OAI.NumericalDimensionOne.finiteType_dimension_trdeg line 142
  4. theorem OAI.NumericalDimensionOne.finiteType_dimension_le_one_iff line 159
  5. theorem OAI.NumericalDimensionOne.affine_functionField_trdeg line 177
  6. theorem OAI.NumericalDimensionOne.coheight_le_one_of_functionField_trdeg line 191
  7. theorem OAI.NumericalDimensionOne.coheight_le_one_of_affine_chart line 230
  8. theorem OAI.NumericalDimensionOne.affine_curve_image line 257
  9. theorem OAI.NumericalDimensionOne.AffineCurveSelection.polynomial_line line 296
  10. theorem OAI.NumericalDimensionOne.AffineCurveSelection.affine_curve_through_point line 362
  11. theorem OAI.NumericalDimensionOne.affine_global_curve_through_point line 444
  12. theorem OAI.NumericalDimensionOne.exists_rationalPoint_with_kernel line 493
  13. theorem OAI.NumericalDimensionOne.closed_curve_through_point_avoiding line 516