OAI/GroupTheory/SimpleAmenable/Simplicial/SimplicialH0.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SimplicialH0.natural line 14
2. def OAI.SimplicialH0.augmentation line 31
3. def OAI.SimplicialH0.connectedIso line 37
4. example OAI.(example at line 53) line 53
5. abbrev OAI.BarHomology.D line 62
6. def OAI.BarHomology.rowIso line 64
7. def OAI.BarHomology.zeroRowIso line 74
8. lemma OAI.BarHomology.zeroRow_vanish line 79
9. lemma OAI.BarHomology.finite_homology line 93
10. lemma OAI.BarHomology.zero_homology line 98
11. lemma OAI.BarHomology.E2_finite line 101
12. lemma OAI.BarHomology.E2_zero line 108
13. lemma OAI.BarHomology.connectivity line 113
14. lemma OAI.BarHomology.finite line 132