OAI/GroupTheory/SimpleAmenable/Homology/RegularAugmentation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuotientRegular.augment line 18
2. lemma OAI.QuotientRegular.augment_single line 27
3. instance OAI.QuotientRegular.augment_epi line 31
4. lemma OAI.QuotientRegular.regular_ext line 36
5. lemma OAI.QuotientRegular.regular_sum_right line 58
6. lemma OAI.QuotientRegular.map_regular_zero line 73
7. lemma OAI.QuotientRegular.map_free_zero line 90
8. instance OAI.QuotientRegular.finite_regular_module line 118
9. lemma OAI.QuotientRegular.H0_finite line 131
10. lemma OAI.QuotientRegular.finite_kernel_H2 line 141