OAI/GroupTheory/SimpleAmenable/Simplicial/PolygonMonoidalData.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.PolygonObject.relabelArrow line 15
  2. def OAI.SimpleAmenable.PolygonObject.sumSwapEquiv line 29
  3. theorem OAI.SimpleAmenable.PolygonObject.sumSwapEquiv_inl line 32
  4. theorem OAI.SimpleAmenable.PolygonObject.sumSwapEquiv_inr line 35
  5. def OAI.SimpleAmenable.PolygonObject.sumSwap line 38
  6. def OAI.SimpleAmenable.PolygonObject.sumAssocEquiv line 53
  7. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_left line 59
  8. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_mid line 62
  9. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_right line 65
  10. def OAI.SimpleAmenable.PolygonObject.sumAssoc line 68
  11. def OAI.SimpleAmenable.PolygonObject.empty line 92
  12. instance OAI.SimpleAmenable.PolygonObject.(instance at line 93) line 93
  13. def OAI.SimpleAmenable.PolygonObject.leftUnitEquiv line 95
  14. def OAI.SimpleAmenable.PolygonObject.rightUnitEquiv line 97
  15. theorem OAI.SimpleAmenable.PolygonObject.leftUnitEquiv_apply line 100
  16. theorem OAI.SimpleAmenable.PolygonObject.rightUnitEquiv_apply line 102
  17. def OAI.SimpleAmenable.PolygonObject.leftUnit line 104
  18. def OAI.SimpleAmenable.PolygonObject.rightUnit line 114
  19. theorem OAI.SimpleAmenable.PolygonObject.sumSwap_apply line 125
  20. theorem OAI.SimpleAmenable.PolygonObject.sumAssoc_apply line 127
  21. theorem OAI.SimpleAmenable.PolygonObject.leftUnit_apply line 129
  22. theorem OAI.SimpleAmenable.PolygonObject.rightUnit_apply line 131
  23. abbrev OAI.SimpleAmenable.PolygonObject.monoidalStruct line 141
  24. instance OAI.SimpleAmenable.PolygonObject.monoidal line 153
  25. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_symm_left line 213
  26. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_symm_mid line 217
  27. theorem OAI.SimpleAmenable.PolygonObject.sumAssocEquiv_symm_right line 221
  28. theorem OAI.SimpleAmenable.PolygonObject.associator_inv_apply line 226
  29. theorem OAI.SimpleAmenable.PolygonObject.sumAssoc_toEquiv line 232
  30. theorem OAI.SimpleAmenable.PolygonObject.inv_arrow_apply line 235
  31. instance OAI.SimpleAmenable.PolygonObject.braided line 240
  32. instance OAI.SimpleAmenable.PolygonObject.symmetric line 281