OAI/GroupTheory/SimpleAmenable/Simplicial/EilenbergZilber.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EilenbergZilber.c line 15
  2. def OAI.EilenbergZilber.diag line 17
  3. def OAI.EilenbergZilber.bisimplicial line 19
  4. def OAI.EilenbergZilber.diagonalIso line 24
  5. def OAI.EilenbergZilber.rowIso line 34
  6. def OAI.EilenbergZilber.bisimplicialIso line 46
  7. def OAI.EilenbergZilber.twoComplex line 60
  8. def OAI.EilenbergZilber.twoIso line 63
  9. def OAI.EilenbergZilber.equiv line 75
  10. def OAI.EilenbergZilber.homologyIso line 80