OAI/GroupTheory/SimpleAmenable/Simplicial/LabelledMonoidal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.sum line 16
2. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.empty line 24
3. lemma OAI.SimpleAmenable.PolygonObject.Labelled.sum_label_left line 29
4. lemma OAI.SimpleAmenable.PolygonObject.Labelled.sum_label_right line 32
5. def OAI.SimpleAmenable.PolygonObject.Labelled.sumHom line 36
6. def OAI.SimpleAmenable.PolygonObject.Labelled.assocHom line 46
7. def OAI.SimpleAmenable.PolygonObject.Labelled.leftHom line 61
8. def OAI.SimpleAmenable.PolygonObject.Labelled.rightHom line 72
9. def OAI.SimpleAmenable.PolygonObject.Labelled.swapHom line 83
10. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 91) line 91
11. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 94) line 94
12. def OAI.SimpleAmenable.PolygonObject.Labelled.inducing line 104
13. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 125) line 125
14. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 126) line 126
15. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 129) line 129
16. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 153) line 153