OAI/GroupTheory/SimpleAmenable/Homology/IntegralHomologyFunctorial.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SimpleAmenable.IntegralHomology.chainsMap2_eq line 17
  2. lemma OAI.SimpleAmenable.IntegralHomology.cyclesMap2_val line 23
  3. theorem OAI.SimpleAmenable.IntegralHomology.mapH2_inner line 28
  4. theorem OAI.SimpleAmenable.IntegralHomology.mapH2_id line 49
  5. theorem OAI.SimpleAmenable.IntegralHomology.mapH2_comp line 55
  6. theorem OAI.SimpleAmenable.IntegralHomology.mapH2_conjugate line 65
  7. abbrev OAI.SimpleAmenable.ConfigurationChains.Chain line 76
  8. def OAI.SimpleAmenable.ConfigurationChains.cone line 78
  9. theorem OAI.SimpleAmenable.ConfigurationChains.cone_single line 81
  10. def OAI.SimpleAmenable.ConfigurationChains.faceSum line 85
  11. def OAI.SimpleAmenable.ConfigurationChains.boundary line 89
  12. theorem OAI.SimpleAmenable.ConfigurationChains.boundary_single line 92
  13. theorem OAI.SimpleAmenable.ConfigurationChains.boundary_cone line 96
  14. theorem OAI.SimpleAmenable.ConfigurationChains.boundary_faceSum line 105
  15. theorem OAI.SimpleAmenable.ConfigurationChains.boundary_boundary line 110
  16. def OAI.SimpleAmenable.ConfigurationChains.vertices line 115
  17. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_zero line 117
  18. theorem OAI.SimpleAmenable.ConfigurationChains.mem_vertices line 119
  19. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_single_subset line 122
  20. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_add_subset line 129
  21. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_neg line 136
  22. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_sub_subset line 139
  23. theorem OAI.SimpleAmenable.ConfigurationChains.cone_support_subset line 142
  24. theorem OAI.SimpleAmenable.ConfigurationChains.vertices_cone_subset line 146
  25. theorem OAI.SimpleAmenable.ConfigurationChains.faceSum_support line 155
  26. theorem OAI.SimpleAmenable.ConfigurationChains.faceSum_support_card line 169