OAI/NumberTheory/PiExponent/Jets/DVRBranchOrder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.DVRBranchOrder.order_eq_addVal line 10
  2. theorem OAI.PiExponent.DVRBranchOrder.injective line 21
  3. theorem OAI.PiExponent.DVRBranchOrder.order_eq_top_iff line 29
  4. theorem OAI.PiExponent.DVRBranchOrder.order_eq_zero_iff_isUnit line 34
  5. theorem OAI.PiExponent.DVRBranchOrder.order_le_iff_dvd line 39
  6. theorem OAI.PiExponent.DVRBranchOrder.order_eq_principal_colength line 45
  7. theorem OAI.PiExponent.DVRBranchOrder.fraction_order_eq_branch_order line 50
  8. theorem OAI.PiExponent.DVRBranchOrder.integerOrder_eq_branch_order line 58
  9. theorem OAI.PiExponent.DVRBranchOrder.algHom_order_eq_addVal line 69
  10. theorem OAI.PiExponent.DVRBranchOrder.algHom_injective line 74