OAI/GroupTheory/SimpleAmenable/Homology/TotalFiniteness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TotalFiniteness.c line 16
2. def OAI.TotalFiniteness.row line 19
3. def OAI.TotalFiniteness.rowIso line 22
4. def OAI.TotalFiniteness.rowHomologyIso line 25
5. lemma OAI.TotalFiniteness.finite line 29
6. lemma OAI.EilenbergZilber.finite_diagonal line 43
7. lemma OAI.FilteredFiniteness.Data.subsingleton_H line 64
8. lemma OAI.E2Leading.subsingleton_E₂ line 108
9. lemma OAI.E2Leading.subsingleton_total_concrete line 116
10. lemma OAI.TotalFiniteness.subsingleton line 133
11. lemma OAI.EilenbergZilber.subsingleton_diagonal line 147