OAI/GroupTheory/SimpleAmenable/Homology/TorusCoefficientFinite.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.SquareStep.OrbitGroupRing line 18
2. def OAI.SimpleAmenable.SquareStep.orbitGroupRing line 20
3. def OAI.SimpleAmenable.SquareStep.periodizeModule line 23
4. theorem OAI.SimpleAmenable.SquareStep.periodizeModule_surjective line 45
5. theorem OAI.SimpleAmenable.SquareStep.orbit_coefficient_finite line 48
6. instance OAI.SimpleAmenable.SquareStep.(instance at line 53) line 53
7. theorem OAI.SimpleAmenable.RingCoinvariants.finite_tensor line 68
8. def OAI.SimpleAmenable.RingCoinvariants.trivialTensorEquiv line 79
9. def OAI.SimpleAmenable.RingCoinvariants.trivialTensorMap line 84
10. theorem OAI.SimpleAmenable.RingCoinvariants.finite_trivialTensor line 95
11. def OAI.SimpleAmenable.SquareStep.coefficientRep line 109
12. theorem OAI.SimpleAmenable.SquareStep.coefficient_homology_finite line 113