OAI/GroupTheory/SimpleAmenable/Simplicial/GroupNerveCoordinates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupNerveCoordinates.labels line 11
  2. def OAI.GroupNerveCoordinates.ofLabels line 13
  3. lemma OAI.GroupNerveCoordinates.labels_ofLabels line 18
  4. lemma OAI.GroupNerveCoordinates.eqToHom_one line 22
  5. lemma OAI.GroupNerveCoordinates.ofLabels_labels line 23
  6. def OAI.GroupNerveCoordinates.equiv line 31
  7. lemma OAI.GroupNerveCoordinates.labels_zero_face line 37
  8. lemma OAI.GroupNerveCoordinates.labels_succ_face line 41
  9. lemma OAI.GroupNerveCoordinates.labels_map line 53
  10. def OAI.GroupNerveCoordinates.chainCoordinates line 70
  11. lemma OAI.GroupNerveCoordinates.coordinates_single line 74
  12. lemma OAI.GroupNerveCoordinates.coordinates_d line 77
  13. def OAI.GroupNerveCoordinates.chainIso line 121
  14. def OAI.GroupNerveCoordinates.homologyIso line 126
  15. lemma OAI.FreeChains.complexIso_natural line 138
  16. lemma OAI.GroupNerveCoordinates.coordinates_natural line 148
  17. lemma OAI.GroupNerveCoordinates.chainIso_natural line 167
  18. lemma OAI.GroupNerveCoordinates.homologyIso_natural line 172