OAI/GroupTheory/SimpleAmenable/Homology/DoubleCoordinates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DoubleCoordinates.Index line 11
  2. def OAI.DoubleCoordinates.toSplit line 12
  3. def OAI.DoubleCoordinates.ofSplit line 15
  4. lemma OAI.DoubleCoordinates.payload_heq line 17
  5. lemma OAI.DoubleCoordinates.left_inv line 21
  6. lemma OAI.DoubleCoordinates.right_inv line 30
  7. def OAI.DoubleCoordinates.equiv line 33
  8. def OAI.DoubleCoordinates.words line 38
  9. lemma OAI.DoubleCoordinates.center line 40
  10. def OAI.RegularLabels.totalInj line 50
  11. def OAI.RegularLabels.totalDesc line 53
  12. lemma OAI.RegularLabels.totalInj_desc line 57
  13. lemma OAI.RegularLabels.total_hom_ext line 62
  14. def OAI.RegularLabels.totalIsColimit line 69
  15. def OAI.MarkedH1.wordInclude line 83
  16. lemma OAI.MarkedH1.wordInclude_nerve line 87
  17. def OAI.MarkedH1.wordDiagram line 105
  18. lemma OAI.MarkedH1.primitive_eq line 109
  19. lemma OAI.MarkedH1.wordInclude_proj line 138
  20. def OAI.MarkedH1.oneIncludeIso line 143
  21. def OAI.MarkedH1.binaryLeft line 153
  22. def OAI.MarkedH1.binaryRight line 164
  23. def OAI.MarkedH1.binaryLeftTranslate line 175
  24. def OAI.MarkedH1.binaryRightTranslate line 180
  25. lemma OAI.MarkedH1.binary_primitive_face line 184
  26. lemma OAI.MarkedH1.binary_primitive_zero line 196
  27. lemma OAI.MarkedH1.binary_primitive_last line 205
  28. lemma OAI.MarkedH1.binary_primitive_zero_other line 214
  29. lemma OAI.MarkedH1.binary_primitive_last_other line 225
  30. lemma OAI.MarkedH1.binary_primitive_middle_stable line 235