OAI/GroupTheory/SimpleAmenable/PolygonGeometry/TranslationRoutingHelpers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PrivateRoutingBank.blockOffsets line 18
2. theorem OAI.SimpleAmenable.PrivateRoutingBank.blockOffsets_apply line 21
3. def OAI.SimpleAmenable.finiteBalancedVector line 45
4. theorem OAI.SimpleAmenable.finiteBalancedVector_apply line 49
5. theorem OAI.SimpleAmenable.finiteBalancedVector_supported line 56
6. theorem OAI.SimpleAmenable.finiteBalancedVector_range line 68
7. theorem OAI.SimpleAmenable.SlotMap_shift_injective line 81
8. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_zero_commute line 100
9. theorem OAI.SimpleAmenable.InitialCoverSystem.privateRoutingFactor_shift_mem line 122
10. theorem OAI.SimpleAmenable.InitialCoverSystem.privateRoutingWord_shift_mem line 147