OAI/NumberTheory/PiExponent/Geometry/CurveContactFamily.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CurveContactFamily.fullCenter line 13
  2. def OAI.PiExponent.CurveContactFamily.fibre line 15
  3. theorem OAI.PiExponent.CurveContactFamily.fullCenter_zero line 17
  4. theorem OAI.PiExponent.CurveContactFamily.fullCenter_succ line 18
  5. theorem OAI.PiExponent.CurveContactFamily.fibre_zero line 19
  6. theorem OAI.PiExponent.CurveContactFamily.fibre_succ line 20
  7. def OAI.PiExponent.CurveContactFamily.places line 24
  8. theorem OAI.PiExponent.CurveContactFamily.mem_places line 31
  9. def OAI.PiExponent.CurveContactFamily.center line 39
  10. theorem OAI.PiExponent.CurveContactFamily.centered line 47
  11. theorem OAI.PiExponent.CurveContactFamily.nonconstant line 56
  12. def OAI.PiExponent.CurveContactFamily.contact line 61
  13. theorem OAI.PiExponent.CurveContactFamily.contact_pos line 76
  14. theorem OAI.PiExponent.CurveContactFamily.contact_nonneg line 90
  15. theorem OAI.PiExponent.CurveContactFamily.logWord_order_lower line 102
  16. theorem OAI.PiExponent.CurveContactFamily.contact_one line 124
  17. theorem OAI.PiExponent.CurveContactFamily.ordinaryWord_order_lower line 146