OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FullGroupAffineData.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.fullGroupSquareShift_exists line 15
  2. def OAI.SimpleAmenable.fullGroupSquareShift line 27
  3. theorem OAI.SimpleAmenable.fullGroupSquareShift_spec line 31
  4. def OAI.SimpleAmenable.fullGroupAffineData line 36
  5. theorem OAI.SimpleAmenable.fullGroupAffineData_chart line 40
  6. theorem OAI.SimpleAmenable.fullGroupAffineData_arrangement line 61
  7. def OAI.SimpleAmenable.flagAffineData line 77
  8. theorem OAI.SimpleAmenable.flagAffineData_chart line 81
  9. theorem OAI.SimpleAmenable.flagAffineData_selected line 91
  10. theorem OAI.SimpleAmenable.flagAffineData_action line 98
  11. theorem OAI.SimpleAmenable.flagAffineData_conjugate line 109
  12. theorem OAI.SimpleAmenable.squareArrangement_finite_range line 124
  13. theorem OAI.SimpleAmenable.flagValue_mem_range line 138
  14. theorem OAI.SimpleAmenable.flagValue_finite_range line 144
  15. theorem OAI.SimpleAmenable.flagAffineData_finite_range line 148
  16. theorem OAI.SimpleAmenable.flagAffineData_bounded line 156
  17. theorem OAI.SimpleAmenable.flagAffineData_separator_control line 165
  18. theorem OAI.SimpleAmenable.flagAffineData_inverse line 175