OAI/Combinatorics/Crossing/PeriodicPolygon.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.cyclicIndex line 8
2. def OAI.Zarankiewicz.periodicPolygon line 10
3. theorem OAI.Zarankiewicz.cyclicIndex_of_lt line 12
4. theorem OAI.Zarankiewicz.cyclicIndex_period line 17
5. theorem OAI.Zarankiewicz.periodicPolygon_closed line 21
6. theorem OAI.Zarankiewicz.cyclicIndex_succ_ne line 25
7. theorem OAI.Zarankiewicz.periodicPolygon_near line 38