OAI/GroupTheory/SimpleAmenable/Homology/RingGroupHomology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.RingCoinvariants.augmentation line 21
2. theorem OAI.SimpleAmenable.RingCoinvariants.augmentation_of line 24
3. def OAI.SimpleAmenable.RingCoinvariants.augmentationTrivialIso line 28
4. instance OAI.SimpleAmenable.RingCoinvariants.(instance at line 39) line 39
5. def OAI.SimpleAmenable.RingCoinvariants.groupResolution line 44
6. def OAI.SimpleAmenable.RingCoinvariants.complexIso line 52
7. theorem OAI.SimpleAmenable.RingCoinvariants.finite_groupHomology_inverse line 60
8. def OAI.SimpleAmenable.RingCoinvariants.inverseHomologyIso line 90
9. theorem OAI.SimpleAmenable.RingCoinvariants.finite_groupHomology line 108