OAI/GroupTheory/SimpleAmenable/Homology/FullGroupStability.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.TrivialHomology.map line 15
  2. lemma OAI.SimpleAmenable.TrivialHomology.map_id line 18
  3. lemma OAI.SimpleAmenable.TrivialHomology.map_comp line 21
  4. lemma OAI.SimpleAmenable.TrivialHomology.map_congr line 26
  5. lemma OAI.SimpleAmenable.TrivialHomology.isIso_equiv line 28
  6. instance OAI.SimpleAmenable.PolygonPlacement.Configuration.empty_subsingleton line 39
  7. def OAI.SimpleAmenable.PolygonPlacement.Configuration.empty line 42
  8. def OAI.SimpleAmenable.PolygonPlacement.Configuration.emptyIso line 44
  9. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.emptyIso_single line 55
  10. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.augmentation_pointMap line 59
  11. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilizer_H1_isIso line 75
  12. def OAI.SimpleAmenable.PolygonPlacement.Configuration.standardStabilizerEquiv line 85
  13. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.standardStabilizerEquiv_subtype line 89
  14. lemma OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilize_H1_isIso line 93
  15. def OAI.SimpleAmenable.TrivialHomology.abelianizationEquiv line 111
  16. def OAI.SimpleAmenable.TrivialHomology.cycle line 116
  17. lemma OAI.SimpleAmenable.TrivialHomology.abelianizationEquiv_cycle line 119
  18. lemma OAI.SimpleAmenable.TrivialHomology.cycle_map line 127
  19. lemma OAI.SimpleAmenable.TrivialHomology.cycle_eq_zero_iff line 136
  20. lemma OAI.SimpleAmenable.TrivialHomology.commutator_comap_of_mono line 142
  21. lemma OAI.SimpleAmenable.TrivialHomology.H1_isZero_of_perfect line 149