OAI/GroupTheory/SimpleAmenable/Simplicial/TripleBarMaps.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntervalBar.Diagram.map_reindex_unit_app line 14
2. lemma OAI.IntervalBar.Diagram.map_triple_unit_app line 25
3. lemma OAI.IntervalBar.Diagram.map_map_map_reindex line 35
4. lemma OAI.IntervalBar.Diagram.barMap_map_map_reindex line 80
5. lemma OAI.IntervalBar.Diagram.bar₂Map_map_reindex line 90
6. def OAI.IntervalBar.Diagram.rows₃Map line 100
7. def OAI.IntervalBar.Diagram.bar₃Map line 103
8. lemma OAI.IntervalBar.Diagram.bar₃Map_homology_isIso line 105
9. def OAI.SimpleAmenable.PolygonObject.stringEval line 118
10. instance OAI.SimpleAmenable.PolygonObject.(instance at line 123) line 123
11. instance OAI.SimpleAmenable.PolygonObject.(instance at line 125) line 125
12. instance OAI.SimpleAmenable.PolygonObject.(instance at line 144) line 144
13. lemma OAI.SimpleAmenable.PolygonObject.pointShift_sum_left line 148
14. lemma OAI.SimpleAmenable.PolygonObject.pointShift_sum_right line 152
15. lemma OAI.SimpleAmenable.PolygonObject.increments_sum_left line 156
16. lemma OAI.SimpleAmenable.PolygonObject.increments_sum_right line 163
17. def OAI.SimpleAmenable.PolygonObject.Labelled.tensorInitial line 171
18. lemma OAI.SimpleAmenable.PolygonObject.Labelled.tensorInitial_positional line 175
19. lemma OAI.SimpleAmenable.PolygonObject.Labelled.tensorInitial_labels line 178
20. def OAI.SimpleAmenable.PolygonObject.Labelled.tensorLadder line 198
21. lemma OAI.SimpleAmenable.PolygonObject.Labelled.tensorLadder_zero line 201
22. def OAI.SimpleAmenable.PolygonObject.Labelled.unitLadder line 203
23. lemma OAI.SimpleAmenable.PolygonObject.Labelled.unitLadder_zero line 206
24. def OAI.SimpleAmenable.PolygonObject.Labelled.initialIso line 207