OAI/NumberTheory/PiExponent/Geometry/CurveContactSum.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveContactSum.contact_sum_le_of_principal_sum line 15
  2. theorem OAI.PiExponent.CurveContactSum.contact_sum_le_div_of_principal_sum line 48
  3. theorem OAI.PiExponent.CurveContactSum.coordinatePole_eq_zero line 60
  4. theorem OAI.PiExponent.CurveContactSum.coordinatePole_finite_support line 71
  5. theorem OAI.PiExponent.CurveContactSum.exists_constant_of_isAlgebraic line 86
  6. theorem OAI.PiExponent.CurveContactSum.frameWord_field_order_lower line 92
  7. theorem OAI.PiExponent.CurveContactSum.coordinateOrder_constant_eq_zero line 138
  8. def OAI.PiExponent.CurveContactSum.coordinateOrderDivisor line 146
  9. theorem OAI.PiExponent.CurveContactSum.coordinateOrderDivisor_apply line 155
  10. theorem OAI.PiExponent.CurveContactSum.coordinateOrderDivisor_degree_zero line 169
  11. def OAI.PiExponent.CurveContactSum.weightedPoleDivisor line 179
  12. theorem OAI.PiExponent.CurveContactSum.weightedPoleDivisor_apply line 188
  13. def OAI.PiExponent.CurveContactSum.weightedDegree line 193
  14. theorem OAI.PiExponent.CurveContactSum.weightedDegree_nonneg line 198
  15. theorem OAI.PiExponent.CurveContactSum.constants_real_nonneg line 206
  16. theorem OAI.PiExponent.CurveContactSum.polynomial_order_lower line 217
  17. theorem OAI.PiExponent.CurveContactSum.polynomial_contact_sum_le line 231
  18. theorem OAI.PiExponent.CurveContactSum.polynomial_contact_sum_le_div line 252
  19. theorem OAI.PiExponent.CurveContactSum.polynomial_eq_zero_of_excess_contact line 267