OAI/Combinatorics/Crossing/TwoTriangleBasis.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Zarankiewicz.TriangleIndexline 10 - def
OAI.Zarankiewicz.triangleCoordEquivline 12 - def
OAI.Zarankiewicz.monomialVectorline 15 - def
OAI.Zarankiewicz.triangleMatrixline 18 - theorem
OAI.Zarankiewicz.triangleMatrix_evalline 22 - theorem
OAI.Zarankiewicz.triangleMatrix_isUnitline 31 - def
OAI.Zarankiewicz.twoTriangleBasisline 44 - theorem
OAI.Zarankiewicz.twoTriangleBasis_applyline 52