OAI/AlgebraicGeometry/PlaneCurves/LineNormalData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Nested derivatives and normal data for moving lines

  1. theorem OAI.Nagata.Workers.W14.pderiv_one_innerPolynomial line 18
  2. theorem OAI.Nagata.Workers.W14.pderiv_one_nestedToBivariate line 26
  3. theorem OAI.Nagata.Workers.W14.planePolynomialEval_nestedToBivariate line 37
  4. theorem OAI.Nagata.Workers.W14.planePolynomialEval_pderiv_one_nestedToBivariate line 48
  5. def OAI.Nagata.Workers.W14.orderedLineIndex line 69

    Source documentation

    The component containing an ordered mark; all additional marks are on zero.

    def orderedLineIndex (k n : ℕ) (hk : 0 < k) (i : Fin (k*k+n)) : Fin k :=
…
  6. def OAI.Nagata.Workers.W14.orderedLineScalar line 73
  7. theorem OAI.Nagata.Workers.W14.orderedAffinePoint_graph line 76
  8. theorem OAI.Nagata.Workers.W14.orderedLine_graph_injective line 85
  9. theorem OAI.Nagata.Workers.W14.orderedLine_restriction_zero line 91
  10. theorem OAI.Nagata.Workers.W14.lineMark_actual_partial line 96
  11. theorem OAI.Nagata.Workers.W14.markedPoint_actual_partial_ne_zero line 104
  12. theorem OAI.Nagata.Workers.W14.extraPoint_actual_partial_ne_zero line 111
  13. theorem OAI.Nagata.Workers.W14.orderedLine_partial_ne_zero line 118
  14. theorem OAI.Nagata.Workers.W14.lineMark_actual_gradient_velocity line 126