OAI/GroupTheory/SimpleAmenable/Configurations/PolygonFixedTrackProgress.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.source_radius_valid line 15
2. theorem OAI.SimpleAmenable.fixed_track_polygon_progress line 24
3. structure OAI.SimpleAmenable.PolygonPlacement line 46
4. instance OAI.SimpleAmenable.PolygonPlacement.(instance at line 54) line 54
5. theorem OAI.SimpleAmenable.PolygonPlacement.ext line 57
6. def OAI.SimpleAmenable.PolygonPlacement.standard line 62
7. theorem OAI.SimpleAmenable.PolygonPlacement.standard_apply line 73
8. def OAI.SimpleAmenable.PolygonPlacement.postcompose line 76
9. theorem OAI.SimpleAmenable.PolygonPlacement.postcompose_apply line 107
10. instance OAI.SimpleAmenable.PolygonPlacement.(instance at line 110) line 110
11. theorem OAI.SimpleAmenable.PolygonPlacement.smul_apply line 115
12. theorem OAI.SimpleAmenable.PolygonPlacement.range_fiber_polygon line 118
13. def OAI.SimpleAmenable.PolygonPlacement.Apart line 142
14. theorem OAI.SimpleAmenable.PolygonPlacement.apart_symm line 144
15. theorem OAI.SimpleAmenable.PolygonPlacement.apart_iff line 146
16. theorem OAI.SimpleAmenable.PolygonPlacement.apart_smul_iff line 155
17. theorem OAI.SimpleAmenable.PolygonPlacement.standard_apart line 159
18. def OAI.SimpleAmenable.PolygonPlacement.bank line 165