OAI/NumberTheory/PiExponent/Jets/DVRBranchExpansion.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.DVRBranchExpansion.residue_sub_dvd line 15
  2. def OAI.PiExponent.DVRBranchExpansion.remainder line 21
  3. theorem OAI.PiExponent.DVRBranchExpansion.mul_remainder line 23
  4. theorem OAI.PiExponent.DVRBranchExpansion.remainder_add line 29
  5. theorem OAI.PiExponent.DVRBranchExpansion.remainder_smul line 36
  6. theorem OAI.PiExponent.DVRBranchExpansion.remainder_algebraMap line 45
  7. theorem OAI.PiExponent.DVRBranchExpansion.residue_uniformizer line 53
  8. theorem OAI.PiExponent.DVRBranchExpansion.remainder_uniformizer_mul line 59
  9. def OAI.PiExponent.DVRBranchExpansion.remainderLinear line 64
  10. def OAI.PiExponent.DVRBranchExpansion.expansionCoeff line 69
  11. theorem OAI.PiExponent.DVRBranchExpansion.expansionCoeff_zero line 71
  12. theorem OAI.PiExponent.DVRBranchExpansion.expansionCoeff_succ line 73
  13. theorem OAI.PiExponent.DVRBranchExpansion.expansionCoeff_add line 79
  14. theorem OAI.PiExponent.DVRBranchExpansion.expansionCoeff_smul line 84
  15. def OAI.PiExponent.DVRBranchExpansion.expansion line 88
  16. theorem OAI.PiExponent.DVRBranchExpansion.coeff_expansion line 90
  17. theorem OAI.PiExponent.DVRBranchExpansion.expansion_add line 94
  18. theorem OAI.PiExponent.DVRBranchExpansion.expansion_smul line 99
  19. theorem OAI.PiExponent.DVRBranchExpansion.expansion_algebraMap line 104
  20. theorem OAI.PiExponent.DVRBranchExpansion.expansion_rec line 113
  21. theorem OAI.PiExponent.DVRBranchExpansion.remainder_mul line 124
  22. theorem OAI.PiExponent.DVRBranchExpansion.expansion_mul line 132
  23. def OAI.PiExponent.DVRBranchExpansion.expansionHom line 164
  24. theorem OAI.PiExponent.DVRBranchExpansion.constantCoeff_expansionHom line 172
  25. theorem OAI.PiExponent.DVRBranchExpansion.expansionHom_uniformizer line 177