OAI/Combinatorics/Crossing/BivariateCoefficients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Zarankiewicz.BiExponent line 11
2. def OAI.Zarankiewicz.biOfCoeffs line 13
3. theorem OAI.Zarankiewicz.biCoeff_biOfCoeffs line 16
4. theorem OAI.Zarankiewicz.biOfCoeffs_injective line 20
5. theorem OAI.Zarankiewicz.biOfCoeffs_bounded line 26
6. theorem OAI.Zarankiewicz.biEval_biOfCoeffs line 44