OAI/GroupTheory/SimpleAmenable/Simplicial/PolygonPositionalMonoidal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.PolygonObject.positional_comp line 19
2. theorem OAI.SimpleAmenable.PolygonObject.positional_inv line 23
3. theorem OAI.SimpleAmenable.PolygonObject.sumArrow_positional line 28
4. theorem OAI.SimpleAmenable.PolygonObject.sumSwap_positional line 36
5. theorem OAI.SimpleAmenable.PolygonObject.sumAssoc_positional line 42
6. theorem OAI.SimpleAmenable.PolygonObject.leftUnit_positional line 52
7. theorem OAI.SimpleAmenable.PolygonObject.rightUnit_positional line 59
8. def OAI.SimpleAmenable.PolygonObject.positionalProperty line 66
9. instance OAI.SimpleAmenable.PolygonObject.positionalProperty_multiplicative line 69
10. instance OAI.SimpleAmenable.PolygonObject.positionalProperty_monoidal line 73
11. instance OAI.SimpleAmenable.PolygonObject.positionalProperty_braided line 83
12. abbrev OAI.SimpleAmenable.PolygonObject.PositionalCategory line 87