OAI/NumberTheory/PiExponent/Geometry/CurveLocalOrder.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.CurveLocalOrder.length_quotient_span_eq_addVal line 12
  2. def OAI.PiExponent.CurveLocalOrder.enatToIntegerOrder line 23
  3. theorem OAI.PiExponent.CurveLocalOrder.enatToIntegerOrder_top line 28
  4. theorem OAI.PiExponent.CurveLocalOrder.enatToIntegerOrder_natCast line 30
  5. theorem OAI.PiExponent.CurveLocalOrder.enatToIntegerOrder_eq_top_iff line 33
  6. theorem OAI.PiExponent.CurveLocalOrder.enatToIntegerOrder_monotone line 36
  7. def OAI.PiExponent.CurveLocalOrder.localAddValuation line 42
  8. theorem OAI.PiExponent.CurveLocalOrder.localAddValuation_apply line 48
  9. theorem OAI.PiExponent.CurveLocalOrder.localAddValuation_eq_top_iff line 52
  10. theorem OAI.PiExponent.CurveLocalOrder.nonZeroDivisors_le_primeCompl line 58
  11. def OAI.PiExponent.CurveLocalOrder.fractionAddValuation line 66
  12. theorem OAI.PiExponent.CurveLocalOrder.fractionAddValuation_algebraMap line 73
  13. theorem OAI.PiExponent.CurveLocalOrder.fraction_order_eq_principal_colength line 80
  14. theorem OAI.PiExponent.CurveLocalOrder.principal_colength_ne_top line 88
  15. theorem OAI.PiExponent.CurveLocalOrder.integerOrder_field_image_eq_length line 94
  16. theorem OAI.PiExponent.CurveLocalOrder.atPrime_principal_colength line 108
  17. theorem OAI.PiExponent.CurveLocalOrder.ramificationIdx_eq_local_order line 123
  18. theorem OAI.PiExponent.CurveLocalOrder.finite_over_coefficient_field_of_finite_length line 138
  19. theorem OAI.PiExponent.CurveLocalOrder.principal_quotient_finite_over_coefficient_field line 150
  20. theorem OAI.PiExponent.CurveLocalOrder.principal_quotient_finrank_eq_order line 157
  21. def OAI.PiExponent.CurveLocalOrder.residueCoefficientEquiv line 166
  22. def OAI.PiExponent.CurveLocalOrder.residueAugmentation line 173
  23. theorem OAI.PiExponent.CurveLocalOrder.residueAugmentation_algebraMap line 178
  24. theorem OAI.PiExponent.CurveLocalOrder.principal_quotient_finrank_eq_order_of_algClosed line 187