OAI/GroupTheory/SimpleAmenable/Homology/ProductChains.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProductChains.sum_f line 15
  2. abbrev OAI.ProductChains.D line 17
  3. def OAI.ProductChains.product line 19
  4. def OAI.ProductChains.twoFree line 25
  5. def OAI.ProductChains.freeIso line 29
  6. def OAI.ProductChains.rowIso line 37
  7. def OAI.ProductChains.tensorIso line 57
  8. def OAI.ProductChains.homologyIso line 79
  9. instance OAI.ChainTensor.leftAdditive line 96
  10. instance OAI.ChainTensor.rightAdditive line 107
  11. def OAI.ChainTensor.leftDistrib line 118
  12. def OAI.ChainTensor.rightDistrib line 120
  13. abbrev OAI.AugmentedSplit.U line 132
  14. abbrev OAI.AugmentedSplit.red line 134
  15. def OAI.AugmentedSplit.sc line 135
  16. def OAI.AugmentedSplit.splitting line 137
  17. def OAI.AugmentedSplit.iso line 140
  18. lemma OAI.AugmentedSplit.flat line 142
  19. lemma OAI.AugmentedSplit.finite line 150
  20. lemma OAI.AugmentedSplit.uni_isZero line 164
  21. def OAI.AugmentedSplit.homologyIso line 168
  22. lemma OAI.AugmentedSplit.vanishing line 173