OAI/GroupTheory/SimpleAmenable/Homology/ConeHomology.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ConeCoordinates.right_cycle line 17
  2. lemma OAI.ConeCoordinates.fst_cycle line 20
  3. lemma OAI.ConeCoordinates.surjective_of_cone_zero line 28
  4. lemma OAI.ConeCoordinates.injective_of_cone_zero line 49
  5. lemma OAI.ConeCoordinates.cone_subsingleton_of_iso line 82
  6. abbrev OAI.TotalCone.c line 127
  7. abbrev OAI.TotalCone.B line 129
  8. abbrev OAI.TotalCone.f line 130
  9. abbrev OAI.TotalCone.inr line 131
  10. lemma OAI.TotalCone.total_zero line 132
  11. def OAI.TotalCone.h line 138
  12. def OAI.TotalCone.comparison line 145
  13. lemma OAI.TotalCone.right_comparison line 147
  14. lemma OAI.TotalCone.left_comparison line 150
  15. def OAI.TotalCone.inverseFZero line 165
  16. def OAI.TotalCone.inverseFSucc line 168
  17. def OAI.TotalCone.inverseF line 176
  18. lemma OAI.TotalCone.zero_inverse line 179
  19. lemma OAI.TotalCone.succ_inverse line 187
  20. lemma OAI.TotalCone.inr_snd line 194
  21. lemma OAI.TotalCone.inr_fst line 197
  22. lemma OAI.TotalCone.inl_snd line 200
  23. lemma OAI.TotalCone.inl_fst line 203
  24. lemma OAI.TotalCone.decomp line 206
  25. lemma OAI.TotalCone.decomp_zero line 214
  26. lemma OAI.TotalCone.right_inverse line 217
  27. lemma OAI.TotalCone.left_inverse line 230
  28. lemma OAI.TotalCone.comparison_inverse line 235
  29. lemma OAI.TotalCone.inverse_comparison line 249
  30. def OAI.TotalCone.iso line 267