OAI/GroupTheory/SimpleAmenable/Homology/HomologyAdditive.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HomologyAdditive.chainsMap_add line 14
  2. instance OAI.HomologyAdditive.additive line 30
  3. lemma OAI.SimpleAmenable.ConfigurationChains.faceSum_ofFn line 46
  4. def OAI.SimpleAmenable.ConfigurationChains.boundaryRep line 65
  5. abbrev OAI.SimpleAmenable.PolygonPlacement.Configuration.column line 79
  6. def OAI.SimpleAmenable.PolygonPlacement.Configuration.face line 83
  7. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.face_apply line 89
  8. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.face_smul line 92
  9. def OAI.SimpleAmenable.PolygonPlacement.Configuration.faceHom line 95
  10. def OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary line 99
  11. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_chain line 104
  12. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_sum line 110
  13. def OAI.SimpleAmenable.PolygonPlacement.Configuration.facePermutation line 139
  14. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.facePermutation_apply line 142
  15. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.permHom_centralizes line 146
  16. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.permHom_face line 165
  17. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.homology_face_eq line 175
  18. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_two line 188
  19. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_three line 192
  20. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.homology_boundary_two_zero line 198
  21. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.homology_boundary_three line 202
  22. def OAI.SimpleAmenable.PolygonPlacement.Configuration.standardLE line 208
  23. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_square line 212
  24. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_exact line 222
  25. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_zero_eq_face line 237
  26. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_zero_epi line 241
  27. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.face_H0_isIso line 251
  28. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_two_H0_isIso line 257
  29. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.boundary_zero_H1_isIso line 261