OAI/AlgebraicGeometry/NumericalDimension/CurveCoordinates.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Curve Coordinates.

  1. lemma OAI.NumericalDimensionOne.exists_uniform_pow_mul_integer_of_integral_inverse line 15
  2. def OAI.NumericalDimensionOne.PolynomialCurveChart.scalar line 40
  3. def OAI.NumericalDimensionOne.PolynomialCurveChart.germ line 43
  4. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.germ_scalar line 46
  5. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.germ_X line 54
  6. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.generators line 60
  7. lemma OAI.NumericalDimensionOne.nonconstant_inv line 80
  8. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.clear line 86
  9. lemma OAI.NumericalDimensionOne.polynomial_eval_surjective_of_contains line 129
  10. lemma OAI.NumericalDimensionOne.PolynomialCurveChart.clear_reciprocal line 137
  11. structure OAI.NumericalDimensionOne.ProjectiveCurveCoordinates line 146
  12. lemma OAI.NumericalDimensionOne.exists_projectiveCurveCoordinates line 163
  13. def OAI.NumericalDimensionOne.projectiveChartRingHom line 213
  14. def OAI.NumericalDimensionOne.projectiveChartRatio line 220
  15. lemma OAI.NumericalDimensionOne.projectiveChartRingHom_mk line 225
  16. lemma OAI.NumericalDimensionOne.projectiveChartRingHom_ratio line 235
  17. lemma OAI.NumericalDimensionOne.projectiveChartRingHom_constants line 240
  18. lemma OAI.NumericalDimensionOne.projectiveChartRingHom_surjective line 247
  19. lemma OAI.NumericalDimensionOne.projectiveVariable_mem line 278
  20. def OAI.NumericalDimensionOne.projectiveAffineMap line 281
  21. lemma OAI.NumericalDimensionOne.projectiveAffineMap_over line 285
  22. lemma OAI.NumericalDimensionOne.projectiveAffineMap_preimage line 297
  23. lemma OAI.NumericalDimensionOne.projectiveAffineMap_immersion line 316
  24. lemma OAI.NumericalDimensionOne.eval₂_homogeneous_scaling line 334
  25. def OAI.NumericalDimensionOne.homogeneousFieldEval line 360
  26. lemma OAI.NumericalDimensionOne.homogeneousFieldEval_mk line 364
  27. lemma OAI.NumericalDimensionOne.homogeneousFieldEval_awayMap line 370
  28. lemma OAI.NumericalDimensionOne.homogeneousFieldEval_awayMap' line 397
  29. lemma OAI.NumericalDimensionOne.homogeneousFieldPoint_independent line 404
  30. def OAI.NumericalDimensionOne.projectiveFieldMap line 436
  31. lemma OAI.NumericalDimensionOne.projectiveFieldMap_independent line 443
  32. lemma OAI.NumericalDimensionOne.projectiveFieldMap_scaling line 450
  33. lemma OAI.NumericalDimensionOne.projectiveFieldMap_eq_affine line 467
  34. lemma OAI.NumericalDimensionOne.projectiveChartRingHom_naturality line 484
  35. lemma OAI.NumericalDimensionOne.projectiveAffineMap_naturality line 493
  36. lemma OAI.NumericalDimensionOne.projectiveFieldMap_over line 502