OAI/GroupTheory/SimpleAmenable/Homology/FreeChains.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeChains.A line 12
  2. abbrev OAI.FreeChains.Z line 13
  3. abbrev OAI.FreeChains.c line 14
  4. def OAI.FreeChains.forward line 16
  5. def OAI.FreeChains.backward line 18
  6. lemma OAI.FreeChains.ι_forward line 20
  7. lemma OAI.FreeChains.backward_mk line 23
  8. def OAI.FreeChains.iso line 27
  9. def OAI.FreeChains.naturalIso line 46
  10. def OAI.FreeChains.complex line 59
  11. def OAI.FreeChains.complexIso line 61
  12. abbrev OAI.AdditiveFinite.basis line 77
  13. abbrev OAI.AdditiveFinite.I line 78
  14. def OAI.AdditiveFinite.incl line 79
  15. def OAI.AdditiveFinite.proj line 81
  16. lemma OAI.AdditiveFinite.sum_proj_incl line 84
  17. lemma OAI.AdditiveFinite.isZero line 91
  18. lemma OAI.AdditiveFinite.finite line 98
  19. abbrev OAI.TensorCoefficient.c line 122
  20. def OAI.TensorCoefficient.functor line 125
  21. instance OAI.TensorCoefficient.(instance at line 131) line 131
  22. def OAI.TensorCoefficient.unitIso line 138
  23. def OAI.TensorCoefficient.homologyFunctor line 142
  24. instance OAI.TensorCoefficient.(instance at line 145) line 145
  25. def OAI.TensorCoefficient.homologyUnitIso line 149
  26. lemma OAI.TensorCoefficient.shortExact line 153
  27. lemma OAI.TensorCoefficient.free_finite line 160
  28. lemma OAI.TensorCoefficient.free_isZero line 167