OAI/Algebra/FormalGroup/Honda/Target.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HeightThree.HondaTarget.Base line 11
  2. def OAI.HeightThree.HondaTarget.variablePoint line 13
  3. def OAI.HeightThree.HondaTarget.multiplicationSeries line 16
  4. structure OAI.HeightThree.HondaTarget.CoordinateIso line 19
  5. def OAI.HeightThree.HondaTarget.FramedEquivalent line 31
  6. def OAI.HeightThree.HondaTarget.HeightCoordinates line 35
  7. def OAI.HeightThree.HondaTarget.IsUniversal line 44
  8. def OAI.HeightThree.HondaTarget.HasUniversalHeightCoordinates line 53