OAI/GroupTheory/SimpleAmenable/Homology/FullH2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.columnAugmentation_H1_isIso line 12
2. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.face_H1_isIso line 29
3. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_two_H1_isIso line 43
4. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_five line 48
5. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_four_H0_isIso line 55
6. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_zero_H2_isIso line 63
7. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilizer_H2_isIso line 79
8. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilize_H2_isIso line 89
9. lemma OAI.SimpleAmenable.TrivialHomology.abelianization_fg line 106
10. lemma OAI.SimpleAmenable.TrivialHomology.abelianization_ring_noetherian line 116
11. def OAI.SimpleAmenable.PolygonTracks.abelianKernelEquiv line 126
12. lemma OAI.SimpleAmenable.PolygonTracks.finite_alternating_H2_of_full line 131