OAI/NumberTheory/PiExponent/Geometry/CurveCenters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CurveCenters.Centered line 13
  2. theorem OAI.PiExponent.CurveCenters.transcendental_sub_constant line 16
  3. theorem OAI.PiExponent.CurveCenters.exists_transcendental_coordinate line 22
  4. theorem OAI.PiExponent.CurveCenters.finite_centered line 38
  5. theorem OAI.PiExponent.CurveCenters.finite_centered_family line 49
  6. def OAI.PiExponent.CurveCenters.centerPlaces line 59
  7. theorem OAI.PiExponent.CurveCenters.mem_centerPlaces line 66
  8. theorem OAI.PiExponent.CurveCenters.Centered.center_eq line 74
  9. theorem OAI.PiExponent.CurveCenters.Centered.constant_coordinate line 86
  10. theorem OAI.PiExponent.CurveCenters.Centered.coordinate_nonneg line 93
  11. theorem OAI.PiExponent.CurveCenters.center_index_unique_of_constant line 99
  12. theorem OAI.PiExponent.CurveCenters.Centered.exists_nonzero_difference line 107