OAI/GroupTheory/SimpleAmenable/PolygonGeometry/AlignedGroups.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.alignedGroup line 16
2. theorem OAI.SimpleAmenable.alignedGroup_generator line 19
3. theorem OAI.SimpleAmenable.alignedGroup_input line 23
4. theorem OAI.SimpleAmenable.alignedGroup_conjugate line 27
5. theorem OAI.SimpleAmenable.alignedGroup_commute line 41
6. theorem OAI.SimpleAmenable.alignedGroup_map line 55
7. def OAI.SimpleAmenable.SmallConditional line 71
8. instance OAI.SimpleAmenable.(instance at line 74) line 74
9. def OAI.SimpleAmenable.sourceAlignedGroup line 76
10. theorem OAI.SimpleAmenable.source_aligned_disjoint_eventually line 83