OAI/Combinatorics/CompleteCrossing/Angles.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Spoke angles, circle angles, scaling, and coordinate frames.

  1. def OAI.Paper170.complexPoint line 19
  2. lemma OAI.Paper170.complexPoint_injective line 21
  3. lemma OAI.Paper170.complexPoint_zero line 25
  4. lemma OAI.Paper170.complexPoint_smul line 27
  5. lemma OAI.Paper170.complexPoint_ne_zero line 31
  6. lemma OAI.Paper170.spokeAngle_coe line 34
  7. lemma OAI.Paper170.finite_spoke_cut line 40
  8. lemma OAI.Paper170.spokeAngle_eq_smul line 62
  9. lemma OAI.Paper170.spokeAngle_smul line 90
  10. lemma OAI.Paper170.circlePoint_complex line 107
  11. lemma OAI.Paper170.circlePoint_arg line 127
  12. lemma OAI.Paper170.circlePoint_arg_lt line 135
  13. def OAI.Paper170.angleRotation line 141
  14. lemma OAI.Paper170.angleRotation_complex line 145
  15. lemma OAI.Paper170.angleRotation_unit line 150
  16. lemma OAI.Paper170.angleRotation_injective line 161
  17. lemma OAI.Paper170.angleRotation_sign line 167
  18. lemma OAI.Paper170.angleRotation_parameter line 176
  19. theorem OAI.Paper170.signed_chord_formula line 193
  20. lemma OAI.Paper170.outwardSpoke_ne_zero line 231
  21. lemma OAI.Paper170.outwardSpoke_interior line 244
  22. lemma OAI.Paper170.spokeAngle_injective line 271
  23. theorem OAI.Paper170.spoke_orders_exist line 300
  24. theorem OAI.Paper170.complexPoint_similarity line 324
  25. def OAI.Paper170.angleCoordinateFrame line 328
  26. theorem OAI.Paper170.complexPoint_angleCoordinateFrame line 332
  27. theorem OAI.Paper170.angleCoordinateFrame_length line 338
  28. theorem OAI.Paper170.angleCoordinateFrame_ne_zero line 348
  29. theorem OAI.Paper170.angleCoordinateFrame_point line 357