OAI/GroupTheory/SimpleAmenable/Configurations/PolygonStringGroupoid.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.PolygonObject.RawString line 16
  2. def OAI.SimpleAmenable.PolygonObject.ladderProperty line 18
  3. instance OAI.SimpleAmenable.PolygonObject.ladderProperty_multiplicative line 21
  4. instance OAI.SimpleAmenable.PolygonObject.ladderProperty_monoidal line 25
  5. instance OAI.SimpleAmenable.PolygonObject.ladderProperty_braided line 35
  6. abbrev OAI.SimpleAmenable.PolygonObject.StringGroupoid line 39
  7. instance OAI.SimpleAmenable.PolygonObject.stringGroupoid_isIso line 41
  8. instance OAI.SimpleAmenable.PolygonObject.stringGroupoid line 52
  9. def OAI.SimpleAmenable.PolygonObject.stringReindex line 55
  10. theorem OAI.SimpleAmenable.PolygonObject.stringReindex_id line 62
  11. theorem OAI.SimpleAmenable.PolygonObject.stringReindex_comp line 67
  12. instance OAI.SimpleAmenable.PolygonObject.stringReindex_monoidal line 74
  13. def OAI.SimpleAmenable.PolygonObject.baseArrow line 111
  14. theorem OAI.SimpleAmenable.PolygonObject.baseArrow_zero line 114
  15. theorem OAI.SimpleAmenable.PolygonObject.baseArrow_comp line 119
  16. def OAI.SimpleAmenable.PolygonObject.extendLadder line 124
  17. theorem OAI.SimpleAmenable.PolygonObject.extendLadder_zero line 134
  18. theorem OAI.SimpleAmenable.PolygonObject.ladder_ext line 138
  19. theorem OAI.SimpleAmenable.PolygonObject.extendLadder_app_zero line 146
  20. def OAI.SimpleAmenable.PolygonObject.trajectory line 149
  21. theorem OAI.SimpleAmenable.PolygonObject.ladder_preserves_trajectory line 152
  22. theorem OAI.SimpleAmenable.PolygonObject.extendLadder_positional line 164
  23. def OAI.SimpleAmenable.PolygonObject.ladderEquiv line 174