OAI/GroupTheory/SimpleAmenable/Homology/PolygonStableHomology.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PolygonTracks.successorStabilize line 12
2. def OAI.SimpleAmenable.PolygonTracks.fullHomologySequence line 16
3. lemma OAI.SimpleAmenable.PolygonTracks.successor_H1_isIso line 19
4. lemma OAI.SimpleAmenable.PolygonTracks.successor_H2_isIso line 27
5. lemma OAI.SimpleAmenable.PolygonTracks.fullH1_eventuallyConstant line 34
6. lemma OAI.SimpleAmenable.PolygonTracks.fullH2_eventuallyConstant line 41
7. lemma OAI.SimpleAmenable.PolygonTracks.fullH1_colimit_ι_isIso line 49
8. lemma OAI.SimpleAmenable.PolygonTracks.fullH2_colimit_ι_isIso line 54
9. def OAI.SimpleAmenable.PolygonTracks.fullH1_colimitIso line 58
10. def OAI.SimpleAmenable.PolygonTracks.fullH2_colimitIso line 64
11. lemma OAI.SimpleAmenable.PolygonTracks.finite_fullH1_iff_colimit line 70
12. lemma OAI.SimpleAmenable.PolygonTracks.finite_fullH2_iff_colimit line 79