OAI/GroupTheory/SimpleAmenable/CentralCovers/AlphabetAlignedGeneration.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.alphabetHom line 14
2. theorem OAI.SimpleAmenable.alphabet_sign line 18
3. theorem OAI.SimpleAmenable.alphabet_support_subset line 25
4. theorem OAI.SimpleAmenable.alphabet_support_card line 35
5. theorem OAI.SimpleAmenable.alphabet_initial_aligned line 43
6. theorem OAI.SimpleAmenable.alphabet_translate_aligned line 61
7. def OAI.SimpleAmenable.alphabetAlignedBoolean line 83
8. theorem OAI.SimpleAmenable.alphabetAlignedBoolean_initial line 88
9. theorem OAI.SimpleAmenable.alphabetAlignedBoolean_translate line 92
10. theorem OAI.SimpleAmenable.alphabetAlignedBoolean_coordinate line 100
11. theorem OAI.SimpleAmenable.alphabet_polygon_aligned line 109
12. def OAI.SimpleAmenable.HasCentralLaw line 136
13. theorem OAI.SimpleAmenable.hasCentralLaw_iff line 139
14. theorem OAI.SimpleAmenable.hasCentralLaw_iff_modelMap line 150
15. theorem OAI.SimpleAmenable.centralLaw_modelMap_surjective line 164
16. theorem OAI.SimpleAmenable.HasCentralLaw.map line 173
17. theorem OAI.SimpleAmenable.centralLaw_of_quotient line 184