OAI/NumberTheory/SingleFold/EllipticCoordinates.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.PointCompiler.E line 11
  2. instance OAI.SingleFold.PointCompiler.(instance at line 12) line 12
  3. lemma OAI.SingleFold.PointCompiler.equation_iff line 15
  4. structure OAI.SingleFold.PointCompiler.Code line 19
  5. def OAI.SingleFold.PointCompiler.Code.Valid line 24
  6. def OAI.SingleFold.PointCompiler.Code.toPoint line 27
  7. def OAI.SingleFold.PointCompiler.encode line 29
  8. lemma OAI.SingleFold.PointCompiler.encode_valid line 32
  9. lemma OAI.SingleFold.PointCompiler.Code.encode_toPoint line 38
  10. lemma OAI.SingleFold.PointCompiler.encode_toPoint line 48
  11. lemma OAI.SingleFold.PointCompiler.Code.unique line 52
  12. abbrev OAI.SingleFold.PointCompiler.Var line 55
  13. def OAI.SingleFold.PointCompiler.fromTuple line 56
  14. def OAI.SingleFold.PointCompiler.tuple line 58
  15. lemma OAI.SingleFold.PointCompiler.from_tuple line 59
  16. lemma OAI.SingleFold.PointCompiler.tuple_from line 63
  17. lemma OAI.SingleFold.PointCompiler.code_valid_semi line 69
  18. def OAI.SingleFold.PointCompiler.Line line 96
  19. lemma OAI.SingleFold.PointCompiler.line_iff line 98
  20. lemma OAI.SingleFold.PointCompiler.E_addX line 113
  21. lemma OAI.SingleFold.PointCompiler.E_addY line 114
  22. lemma OAI.SingleFold.PointCompiler.E_negY line 115
  23. lemma OAI.SingleFold.PointCompiler.line_chord line 117
  24. lemma OAI.SingleFold.PointCompiler.line_tangent line 125
  25. def OAI.SingleFold.PointCompiler.AddEq line 138
  26. lemma OAI.SingleFold.PointCompiler.encode_injective line 147
  27. lemma OAI.SingleFold.PointCompiler.addEq_encode line 153
  28. lemma OAI.SingleFold.PointCompiler.addEq_spec line 194
  29. lemma OAI.SingleFold.PointCompiler.addition_existsUnique line 197
  30. def OAI.SingleFold.PointCompiler.At line 209
  31. def OAI.SingleFold.PointCompiler.AllValid line 210
  32. lemma OAI.SingleFold.PointCompiler.allValid_semi line 211
  33. lemma OAI.SingleFold.PointCompiler.flag_semi line 214
  34. lemma OAI.SingleFold.PointCompiler.codeEq_semi line 217
  35. def OAI.SingleFold.PointCompiler.ratMap line 229
  36. def OAI.SingleFold.PointCompiler.values line 230
  37. def OAI.SingleFold.PointCompiler.xe line 231
  38. def OAI.SingleFold.PointCompiler.ye line 232
  39. lemma OAI.SingleFold.PointCompiler.allValid_rational line 234
  40. lemma OAI.SingleFold.PointCompiler.exprEq_semi line 239
  41. lemma OAI.SingleFold.PointCompiler.exprNe_semi line 241
  42. lemma OAI.SingleFold.PointCompiler.line_semi line 243
  43. lemma OAI.SingleFold.PointCompiler.chord_semi line 251
  44. lemma OAI.SingleFold.PointCompiler.tangent_semi line 258
  45. lemma OAI.SingleFold.PointCompiler.xeq_semi line 265
  46. lemma OAI.SingleFold.PointCompiler.xne_semi line 266
  47. lemma OAI.SingleFold.PointCompiler.yneg_semi line 267
  48. lemma OAI.SingleFold.PointCompiler.ynneg_semi line 268
  49. lemma OAI.SingleFold.PointCompiler.add1_semi line 271
  50. lemma OAI.SingleFold.PointCompiler.add2_semi line 274
  51. lemma OAI.SingleFold.PointCompiler.add3_semi line 276
  52. lemma OAI.SingleFold.PointCompiler.add4_semi line 280
  53. lemma OAI.SingleFold.PointCompiler.add5_semi line 286
  54. lemma OAI.SingleFold.PointCompiler.addEq_semi line 292
  55. lemma OAI.SingleFold.PointCompiler.fromTuple_injective line 302
  56. def OAI.SingleFold.PointCompiler.MulRel line 307
  57. lemma OAI.SingleFold.PointCompiler.mulRel_valid line 308
  58. lemma OAI.SingleFold.PointCompiler.mulRel_unique line 311
  59. lemma OAI.SingleFold.PointCompiler.mulRel_exists line 315
  60. lemma OAI.SingleFold.PointCompiler.mulRel_zero line 319
  61. lemma OAI.SingleFold.PointCompiler.mulRel_succ line 323
  62. lemma OAI.SingleFold.PointCompiler.valid_sf line 338
  63. lemma OAI.SingleFold.PointCompiler.const_sf line 339
  64. def OAI.SingleFold.PointCompiler.tripleMap line 348
  65. lemma OAI.SingleFold.PointCompiler.add_general_sf line 349
  66. lemma OAI.SingleFold.PointCompiler.mulRel_sf line 367
  67. theorem OAI.SingleFold.Compiler.Semi.max_eq line 402
  68. def OAI.SingleFold.PointCompiler.Code.height line 415
  69. lemma OAI.SingleFold.PointCompiler.height_pos line 416
  70. lemma OAI.SingleFold.PointCompiler.height_semi line 418
  71. def OAI.SingleFold.PointCompiler.WRel line 428
  72. lemma OAI.SingleFold.PointCompiler.wRel_semantics line 429
  73. lemma OAI.SingleFold.PointCompiler.wRel_unique line 434
  74. lemma OAI.SingleFold.PointCompiler.wRel_exists line 438
  75. lemma OAI.SingleFold.PointCompiler.wRel_sf line 441
  76. lemma OAI.SingleFold.PointCompiler.rational_height line 452