OAI/Combinatorics/Crossing/WalkVectorSum.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.walkEdgeChain_sum_stepsline 12 - theorem
OAI.Zarankiewicz.walkEdgeChain_sum_cyclic_dartsline 21 - theorem
OAI.Zarankiewicz.edgePairing_sum_leftline 31 - theorem
OAI.Zarankiewicz.edgePairing_sum_rightline 39 - theorem
OAI.Zarankiewicz.edgePairing_smul_singleline 47 - theorem
OAI.Zarankiewicz.edgePairing_walk_dart_sumline 52