OAI/GroupTheory/SimpleAmenable/Homology/MarkedSigns.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkedSigns.exponent line 9
  2. lemma OAI.MarkedSigns.triangular_step line 10
  3. lemma OAI.MarkedSigns.vertical_step line 14
  4. lemma OAI.MarkedSigns.horizontal_step line 17
  5. lemma OAI.MarkedSigns.vertical line 21
  6. lemma OAI.MarkedSigns.square line 26
  7. lemma OAI.MarkedSigns.horizontal line 28
  8. abbrev OAI.MarkedH1.H line 52
  9. def OAI.MarkedH1.isColimit line 53
  10. def OAI.MarkedH1.signIso line 58
  11. def OAI.MarkedH1.labelIso line 65
  12. def OAI.MarkedH1.labelDiagramIso line 68
  13. def OAI.MarkedH1.reindexedCofan line 73
  14. def OAI.MarkedH1.labelledCofan line 76
  15. def OAI.MarkedH1.labelledIsColimit line 77
  16. def OAI.MarkedH1.gradedIso line 81
  17. lemma OAI.MarkedH1.totalInj_gradedIso line 86