OAI/GroupTheory/SimpleAmenable/Homology/AlternatingH2.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.PolygonPlacement.Configuration.altEmptyIso line 16
  2. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.altEmptyIso_single line 20
  3. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.altAugmentation_pointMap line 22
  4. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.alternatingStabilizer_H2_epi line 38
  5. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilizeAlternating_H2_epi line 51
  6. def OAI.SimpleAmenable.PolygonTracks.castAlternating line 60
  7. lemma OAI.SimpleAmenable.PolygonTracks.castAlternating_val line 63
  8. lemma OAI.SimpleAmenable.PolygonTracks.stabilizeAlternating_add line 66
  9. lemma OAI.SimpleAmenable.PolygonTracks.stabilizeAlternating_zero_bijective line 77
  10. lemma OAI.SimpleAmenable.PolygonTracks.stabilizeAlternating_H2_epi line 89
  11. lemma OAI.SimpleAmenable.PolygonTracks.stabilizeAlternating_mapH2_surjective line 108
  12. lemma OAI.SimpleAmenable.PolygonTracks.fullAction_trivial line 113
  13. lemma OAI.FiniteHomologyReturn.finite_of_exact line 131
  14. lemma OAI.FiniteHomologyReturn.finite_range_of_exact line 141
  15. lemma OAI.FiniteHomologyReturn.finite_H2 line 176