OAI/GroupTheory/SimpleAmenable/Configurations/FiberAddition.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.BarFiberProduct.prodFunctorBraided line 16
2. lemma OAI.IntervalBar.Diagram.bar₃Map_id_homology line 32
3. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.merge line 43
4. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.(instance at line 45) line 45
5. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.selected line 46
6. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.selectedMonoidal line 51
7. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.selectedBraided line 53
8. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.insertFiber line 55
9. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.(instance at line 57) line 57
10. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.insertCoordinate line 58
11. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.(instance at line 59) line 59
12. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.selected_homology line 67
13. def OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.mergeInsertIso line 81
14. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.merge_μ line 93
15. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.mergeInsert_false_μ line 104
16. lemma OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.mergeInsert_true_μ line 110
17. instance OAI.SimpleAmenable.PolygonObject.FiniteSetGroupoid.mergeInsertMonoidal line 116