OAI/GroupTheory/SimpleAmenable/PolygonGeometry/SmallControlCalculus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.ControlAlphabet line 17
2. instance OAI.SimpleAmenable.controlAlphabet_perfect line 20
3. abbrev OAI.SimpleAmenable.TrackStar line 23
4. def OAI.SimpleAmenable.SmallSupported line 26
5. def OAI.SimpleAmenable.SmallControlled line 29
6. theorem OAI.SimpleAmenable.five_bank_of_card line 36
7. theorem OAI.SimpleAmenable.small_star_representative line 53
8. theorem OAI.SimpleAmenable.small_control_transfer line 65