OAI/GroupTheory/SimpleAmenable/Homology/RegularBlock.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RegularCoefficient.block line 13
  2. lemma OAI.RegularCoefficient.block_hom_ext line 16
  3. def OAI.RegularCoefficient.blockDesc line 23
  4. lemma OAI.RegularCoefficient.block_desc line 27
  5. def OAI.RegularCoefficient.totalBlock line 36
  6. lemma OAI.RegularCoefficient.totalBlock_hom_ext line 40
  7. def OAI.RegularCoefficient.totalBlockDesc line 47
  8. lemma OAI.RegularCoefficient.totalBlock_desc line 51
  9. abbrev OAI.RegularLabels.W line 63
  10. abbrev OAI.RegularLabels.fiber line 64
  11. lemma OAI.RegularLabels.rightEq line 65
  12. def OAI.RegularLabels.inj line 69
  13. def OAI.RegularLabels.desc line 73
  14. lemma OAI.RegularLabels.include_desc line 76
  15. lemma OAI.RegularLabels.hom_ext line 89
  16. def OAI.RegularLabels.isColimit line 100
  17. abbrev OAI.MarkedCoordinates.Split line 109
  18. def OAI.MarkedCoordinates.word line 110
  19. lemma OAI.MarkedCoordinates.word_center line 113
  20. lemma OAI.MarkedCoordinates.word_left line 115
  21. lemma OAI.MarkedCoordinates.word_right line 117
  22. def OAI.MarkedCoordinates.vertical line 124
  23. def OAI.MarkedCoordinates.horizontal line 125
  24. lemma OAI.MarkedCoordinates.word_recover line 126
  25. lemma OAI.MarkedCoordinates.vertical_word line 137
  26. lemma OAI.MarkedCoordinates.horizontal_word line 139
  27. def OAI.MarkedCoordinates.equiv line 141