OAI/GroupTheory/SimpleAmenable/Configurations/PolygonPlacementAlternating.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.PolygonPlacement.permHom_mem_alternating line 19
2. theorem OAI.SimpleAmenable.PolygonPlacement.familyPerm_mem_alternating line 65
3. theorem OAI.SimpleAmenable.PolygonPlacement.alternating_move_to_bank line 74
4. theorem OAI.SimpleAmenable.PolygonPlacement.alternating_configuration_transitive line 109
5. def OAI.SimpleAmenable.PolygonPlacement.Configuration line 141
6. instance OAI.SimpleAmenable.PolygonPlacement.Configuration.(instance at line 146) line 146
7. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.ext line 148
8. instance OAI.SimpleAmenable.PolygonPlacement.Configuration.(instance at line 151) line 151
9. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.smul_apply line 156
10. def OAI.SimpleAmenable.PolygonPlacement.Configuration.standard line 159
11. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.standard_apply line 166
12. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.stabilizer_standard line 169
13. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.transitive line 184
14. def OAI.SimpleAmenable.PolygonPlacement.Configuration.quotientStabilizerEquiv line 189
15. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.quotientStabilizerEquiv_apply line 198
16. def OAI.SimpleAmenable.PolygonPlacement.Configuration.quotientBankEquiv line 202
17. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.quotientBankEquiv_apply line 207
18. theorem OAI.SimpleAmenable.PolygonPlacement.Configuration.quotientBankEquiv_smul line 211