OAI/Combinatorics/Crossing/CycleMatrixBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.leftHalfOrder line 11
2. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.rightHalfOrder line 14
3. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.flagPairing_left_block line 17
4. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.flagPairing_right_block line 31
5. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.cycleIntersectionMatrix_entry line 45
6. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.cycleIntersectionMatrix_diagonal_block line 51
7. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.cycleIntersectionMatrix_offDiagonal_block line 59