OAI/GroupTheory/SimpleAmenable/Homology/PolygonCoefficientFinite.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.planeCornerLinear line 15
  2. theorem OAI.SimpleAmenable.planeCornerCoordinates_translate line 31
  3. def OAI.SimpleAmenable.planeCornerEmbedding line 42
  4. theorem OAI.SimpleAmenable.planeCornerEmbedding_injective line 56
  5. theorem OAI.SimpleAmenable.polygon_coefficient_finite line 66
  6. instance OAI.SimpleAmenable.(instance at line 70) line 70
  7. instance OAI.SimpleAmenable.(instance at line 72) line 72
  8. instance OAI.SimpleAmenable.(instance at line 74) line 74
  9. theorem OAI.SimpleAmenable.polygon_coefficient_module_finite line 77
  10. theorem OAI.SimpleAmenable.NoetherianResolution.fg_projective_of_free line 89
  11. theorem OAI.SimpleAmenable.NoetherianResolution.finitePresentation line 100
  12. theorem OAI.SimpleAmenable.NoetherianResolution.forget_projective line 112
  13. def OAI.SimpleAmenable.NoetherianResolution.resolution line 129
  14. instance OAI.SimpleAmenable.NoetherianResolution.finite_resolution line 133
  15. theorem OAI.SimpleAmenable.NoetherianResolution.finite_short_homology line 137
  16. theorem OAI.SimpleAmenable.NoetherianResolution.finite_homology line 147