OAI/GroupTheory/SimpleAmenable/Homology/NoetherianTor.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.NoetherianResolution.homologyMap_smul line 19
  2. def OAI.SimpleAmenable.NoetherianResolution.annihilatorHomotopy line 26
  3. theorem OAI.SimpleAmenable.NoetherianResolution.annihilator_homology line 36
  4. theorem OAI.SimpleAmenable.NoetherianResolution.finite_tensor_resolution_homology line 49
  5. theorem OAI.SimpleAmenable.module_finite_int_of_augmentation line 61
  6. abbrev OAI.SimpleAmenable.NoetherianResolution.augmentationModule line 84
  7. instance OAI.SimpleAmenable.NoetherianResolution.finite_augmentationModule line 87
  8. def OAI.SimpleAmenable.NoetherianResolution.augmentationResolution line 92
  9. def OAI.SimpleAmenable.NoetherianResolution.augmentationComplex line 96
  10. instance OAI.SimpleAmenable.NoetherianResolution.finite_augmentation_homology line 101
  11. theorem OAI.SimpleAmenable.NoetherianResolution.augmentation_homology_smul line 105
  12. theorem OAI.SimpleAmenable.NoetherianResolution.finite_int_augmentation_homology line 118
  13. theorem OAI.SimpleAmenable.NoetherianResolution.finite_int_Tor_augmentation line 122
  14. abbrev OAI.SimpleAmenable.RingCoinvariants.inverseRep line 144
  15. abbrev OAI.SimpleAmenable.RingCoinvariants.moduleRep line 147
  16. theorem OAI.SimpleAmenable.RingCoinvariants.inverseRep_apply line 150
  17. theorem OAI.SimpleAmenable.RingCoinvariants.moduleRep_apply line 153
  18. def OAI.SimpleAmenable.RingCoinvariants.forwardTensor line 156
  19. theorem OAI.SimpleAmenable.RingCoinvariants.forwardTensor_invariant line 160
  20. def OAI.SimpleAmenable.RingCoinvariants.forward line 170
  21. theorem OAI.SimpleAmenable.RingCoinvariants.forward_mk line 176
  22. theorem OAI.SimpleAmenable.RingCoinvariants.mk_act_left line 180
  23. theorem OAI.SimpleAmenable.RingCoinvariants.mk_balanced_group line 193
  24. def OAI.SimpleAmenable.RingCoinvariants.backward line 205
  25. theorem OAI.SimpleAmenable.RingCoinvariants.backward_mk line 220
  26. def OAI.SimpleAmenable.RingCoinvariants.equiv line 224
  27. theorem OAI.SimpleAmenable.RingCoinvariants.equiv_mk line 238
  28. def OAI.SimpleAmenable.RingCoinvariants.moduleRepIso line 242
  29. def OAI.SimpleAmenable.RingCoinvariants.intRestrictionIso line 256
  30. def OAI.SimpleAmenable.RingCoinvariants.functorIso line 271