OAI/GroupTheory/SimpleAmenable/PolygonGeometry/TorusStepFunctions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.squareSign line 15
  2. def OAI.SimpleAmenable.HasSquareArrangement line 18
  3. theorem OAI.SimpleAmenable.polygon_hasSquareArrangement line 21
  4. theorem OAI.SimpleAmenable.squareArrangement_precomp line 37
  5. theorem OAI.SimpleAmenable.squareArrangement_translate line 46
  6. def OAI.SimpleAmenable.squareStepSubmodule line 53
  7. abbrev OAI.SimpleAmenable.SquareStep line 65
  8. def OAI.SimpleAmenable.SquareStep.translate line 70
  9. theorem OAI.SimpleAmenable.SquareStep.translate_apply line 76
  10. theorem OAI.SimpleAmenable.SquareStep.translate_zero line 79
  11. theorem OAI.SimpleAmenable.SquareStep.translate_add line 84
  12. def OAI.SimpleAmenable.SquareStep.representation line 90
  13. def OAI.SimpleAmenable.SquareStep.restrict line 96
  14. theorem OAI.SimpleAmenable.SquareStep.restrict_apply line 103
  15. def OAI.SimpleAmenable.SquareStep.InSquare line 115
  16. def OAI.SimpleAmenable.SquareStep.squareEdgeCuts line 118
  17. theorem OAI.SimpleAmenable.SquareStep.square_signs line 120
  18. def OAI.SimpleAmenable.SquareStep.extendFun line 140
  19. theorem OAI.SimpleAmenable.SquareStep.extend_arrangement line 143
  20. theorem OAI.SimpleAmenable.SquareStep.extend_compact line 154
  21. def OAI.SimpleAmenable.SquareStep.extend line 162
  22. theorem OAI.SimpleAmenable.SquareStep.extend_apply line 175
  23. theorem OAI.SimpleAmenable.SquareStep.restrict_extend line 178
  24. def OAI.SimpleAmenable.SquareStep.intPair line 183
  25. theorem OAI.SimpleAmenable.SquareStep.intPair_zero line 185
  26. theorem OAI.SimpleAmenable.SquareStep.intPair_add line 186
  27. theorem OAI.SimpleAmenable.SquareStep.intPair_neg line 188
  28. def OAI.SimpleAmenable.SquareStep.slice line 191
  29. theorem OAI.SimpleAmenable.SquareStep.slice_apply line 194
  30. theorem OAI.SimpleAmenable.SquareStep.slice_zero line 199