OAI/NumberTheory/PiExponent/Jets/DVRBranch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.DVRBranch.residueCoefficientMap line 14
  2. theorem OAI.PiExponent.DVRBranch.residueCoefficientMap_ker line 18
  3. def OAI.PiExponent.DVRBranch.uniformizer line 26
  4. theorem OAI.PiExponent.DVRBranch.uniformizer_irreducible line 28
  5. theorem OAI.PiExponent.DVRBranch.residueCoefficientMap_ker_span line 31
  6. def OAI.PiExponent.DVRBranch.expansion line 35
  7. theorem OAI.PiExponent.DVRBranch.expansion_uniformizer line 39
  8. theorem OAI.PiExponent.DVRBranch.expansion_order line 42
  9. theorem OAI.PiExponent.DVRBranch.expansion_injective line 47
  10. theorem OAI.PiExponent.DVRBranch.expansion_constantCoeff line 51
  11. theorem OAI.PiExponent.DVRBranch.expansion_order_eq_length line 55