OAI/NumberTheory/PiExponent/Geometry/WeightedCurveDegree.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.WeightedCurveDegree.integerOrder line 9
  2. theorem OAI.PiExponent.WeightedCurveDegree.coe_integerOrder line 13
  3. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_one line 17
  4. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_mul line 22
  5. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_pow line 28
  6. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_prod line 35
  7. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_monomial line 43
  8. def OAI.PiExponent.WeightedCurveDegree.weightedPole line 48
  9. theorem OAI.PiExponent.WeightedCurveDegree.weightedPole_nonneg line 53
  10. theorem OAI.PiExponent.WeightedCurveDegree.div_le_weightedPole line 58
  11. theorem OAI.PiExponent.WeightedCurveDegree.monomial_pole_le line 63
  12. theorem OAI.PiExponent.WeightedCurveDegree.monomial_max_pole_eq line 84
  13. theorem OAI.PiExponent.WeightedCurveDegree.valuation_monomial_max_pole_eq line 116
  14. def OAI.PiExponent.WeightedCurveDegree.monomialPoleCoefficient line 131
  15. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleCoefficient_nonneg line 137
  16. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleCoefficient_eq line 145
  17. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleCoefficient_eq_zero line 161
  18. def OAI.PiExponent.WeightedCurveDegree.monomialPoleDivisor line 171
  19. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleDivisor_apply line 183
  20. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleDivisor_effective line 194
  21. theorem OAI.PiExponent.WeightedCurveDegree.monomialPoleDivisor_degree_eq line 204
  22. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_inv line 223
  23. theorem OAI.PiExponent.WeightedCurveDegree.integerOrder_div line 229
  24. theorem OAI.PiExponent.WeightedCurveDegree.mem_valuationSubring_iff_order_nonneg line 234
  25. theorem OAI.PiExponent.WeightedCurveDegree.exists_regular_monomial_chart line 241