OAI/GroupTheory/SimpleAmenable/CentralCovers/PerfectGeneratingFamilies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.perfect_iSup line 17
  2. theorem OAI.SimpleAmenable.central_perfect_generating_ranges line 26
  3. theorem OAI.SimpleAmenable.universal_generating_ranges line 46
  4. def OAI.SimpleAmenable.translationWordMap line 63
  5. theorem OAI.SimpleAmenable.translationWordMap_surjective line 67
  6. theorem OAI.SimpleAmenable.translation_lattice_fg line 82
  7. theorem OAI.SimpleAmenable.translation_centralizers_eventually line 86
  8. def OAI.SimpleAmenable.sourceLatticeMap line 149
  9. theorem OAI.SimpleAmenable.source_centralizing_translation_lifts_eventually line 155