OAI/GroupTheory/SimpleAmenable/Amenability/SubgroupTestReiter.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.subgroupOrbitSetoid line 15
  2. def OAI.SimpleAmenable.subgroupOrbitBase line 27
  3. theorem OAI.SimpleAmenable.subgroupOrbitBase_spec line 30
  4. def OAI.SimpleAmenable.subgroupCoordinate line 34
  5. theorem OAI.SimpleAmenable.subgroupCoordinate_spec line 37
  6. theorem OAI.SimpleAmenable.subgroupCoordinate_mul line 40
  7. theorem OAI.SimpleAmenable.finite_weights_push line 50
  8. theorem OAI.SimpleAmenable.FiniteTestReiter.subgroup line 60
  9. theorem OAI.SimpleAmenable.polygonFullGroup_folner line 76
  10. theorem OAI.SimpleAmenable.polygonAlternatingGroup_folner line 80
  11. theorem OAI.SimpleAmenable.polygon_infinite_simple_folner line 85