OAI/Combinatorics/Crossing/TriangleFactorization.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Zarankiewicz.triangleDiagonalWeightline 10 - theorem
OAI.Zarankiewicz.triangleDiagonalWeight_ne_zeroline 14 - theorem
OAI.Zarankiewicz.rankDetector_triangle_sumline 26 - theorem
OAI.Zarankiewicz.rankDetector_triangle_factorizationline 46 - theorem
OAI.Zarankiewicz.rankDetector_ordered_isUnitline 60