OAI/GroupTheory/SimpleAmenable/Configurations/TrackTranslationChart.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.trackTranslationChart line 13
  2. theorem OAI.SimpleAmenable.trackTranslation_hasTable line 17
  3. def OAI.SimpleAmenable.trackTranslation line 29
  4. theorem OAI.SimpleAmenable.trackTranslation_apply line 32
  5. theorem OAI.SimpleAmenable.trackTranslation_zero line 36
  6. theorem OAI.SimpleAmenable.trackTranslation_add line 43
  7. theorem OAI.SimpleAmenable.trackTranslation_neg line 52
  8. theorem OAI.SimpleAmenable.trackTranslation_sub line 59
  9. def OAI.SimpleAmenable.wholePolygon line 63
  10. theorem OAI.SimpleAmenable.constant_conjugate_translation line 66
  11. theorem OAI.SimpleAmenable.constant_conjugate_point_translation line 78
  12. theorem OAI.SimpleAmenable.trackTranslation_difference_mem line 90
  13. def OAI.SimpleAmenable.coordinatePrimitive line 116
  14. def OAI.SimpleAmenable.circularBoxPiece line 122
  15. def OAI.SimpleAmenable.clippedSlopePrimitive line 134
  16. def OAI.SimpleAmenable.initialTest line 143
  17. def OAI.SimpleAmenable.SourceGeneratorLabel line 147
  18. instance OAI.SimpleAmenable.(instance at line 151) line 151
  19. def OAI.SimpleAmenable.sourceGenerator line 155
  20. theorem OAI.SimpleAmenable.sourceGenerator_mem line 162
  21. def OAI.SimpleAmenable.alternatingGenerator line 168