OAI/GroupTheory/SimpleAmenable/Simplicial/TranslationNerve.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TranslationNerve.C line 13
  2. abbrev OAI.TranslationNerve.B line 14
  3. lemma OAI.TranslationNerve.eqToHom_val line 15
  4. lemma OAI.TranslationNerve.single_eqToHom line 16
  5. def OAI.TranslationNerve.lift line 17
  6. lemma OAI.TranslationNerve.lift_left line 29
  7. lemma OAI.TranslationNerve.lift_project line 34
  8. lemma OAI.TranslationNerve.lift_recover line 38
  9. def OAI.TranslationNerve.coordinates line 48
  10. def OAI.TranslationNerve.translate line 53
  11. lemma OAI.TranslationNerve.translate_one line 61
  12. lemma OAI.TranslationNerve.translate_mul line 68
  13. instance OAI.TranslationNerve.action line 75
  14. lemma OAI.TranslationNerve.smul_left line 79
  15. lemma OAI.TranslationNerve.smul_project line 81
  16. lemma OAI.TranslationNerve.smul_lift line 86
  17. def OAI.TranslationNerve.simplicial line 94
  18. def OAI.TranslationNerve.actionCoordinates line 111
  19. def OAI.TranslationNerve.linear line 117
  20. def OAI.TranslationNerve.complex line 118
  21. def OAI.TranslationNerve.freeIso line 119
  22. instance OAI.TranslationNerve.projective line 125
  23. abbrev OAI.TranslationNerve.forgetRep line 127
  24. def OAI.TranslationNerve.coeffIso line 128
  25. lemma OAI.TranslationNerve.coeff_natural line 130
  26. lemma OAI.TranslationNerve.coeff_d line 135
  27. def OAI.TranslationNerve.forgetIso line 149
  28. def OAI.TranslationNerve.aug0 line 154
  29. lemma OAI.TranslationNerve.d_aug0 line 167
  30. def OAI.TranslationNerve.aug line 176
  31. lemma OAI.TranslationNerve.forget_aug line 178
  32. instance OAI.TranslationNerve.nerve_aug_quasiIso line 184
  33. instance OAI.TranslationNerve.aug_quasiIso line 197
  34. def OAI.TranslationNerve.resolution line 204