OAI/NumberTheory/PiExponent/Geometry/PlaceCenteredBranch.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.PlaceCenteredBranch.lift line 15
  2. theorem OAI.PiExponent.PlaceCenteredBranch.lift_coe line 19
  3. theorem OAI.PiExponent.PlaceCenteredBranch.lift_nonconstant line 22
  4. theorem OAI.PiExponent.PlaceCenteredBranch.lift_eq_algebraMap_iff line 30
  5. theorem OAI.PiExponent.PlaceCenteredBranch.lift_aeval line 38
  6. theorem OAI.PiExponent.PlaceCenteredBranch.coordinateOrder_aeval_eq_length line 45
  7. theorem OAI.PiExponent.PlaceCenteredBranch.lift_residue line 67
  8. theorem OAI.PiExponent.PlaceCenteredBranch.logLift_nonconstant line 82
  9. def OAI.PiExponent.PlaceCenteredBranch.logContact line 92
  10. theorem OAI.PiExponent.PlaceCenteredBranch.logContact_pos line 99
  11. def OAI.PiExponent.PlaceCenteredBranch.ordinaryContact line 107
  12. theorem OAI.PiExponent.PlaceCenteredBranch.ordinaryContact_pos line 112
  13. theorem OAI.PiExponent.PlaceCenteredBranch.logWord_field_order_lower line 117
  14. theorem OAI.PiExponent.PlaceCenteredBranch.ordinaryWord_field_order_lower line 146
  15. theorem OAI.PiExponent.PlaceCenteredBranch.fibre_nonconstant line 164
  16. theorem OAI.PiExponent.PlaceCenteredBranch.logContact_one line 173