OAI/Combinatorics/Crossing/Bivariate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Zarankiewicz.BiPoly line 11
  2. def OAI.Zarankiewicz.biCoeff line 13
  3. def OAI.Zarankiewicz.biEval line 15
  4. def OAI.Zarankiewicz.BiBounded line 17
  5. def OAI.Zarankiewicz.flattenBi line 20
  6. theorem OAI.Zarankiewicz.flattenBi_apply line 25
  7. def OAI.Zarankiewicz.swapBi line 27
  8. theorem OAI.Zarankiewicz.biCoeff_swap line 31
  9. theorem OAI.Zarankiewicz.bi_ext line 37
  10. theorem OAI.Zarankiewicz.swapBi_swapBi line 45
  11. theorem OAI.Zarankiewicz.swapBi_single line 50
  12. theorem OAI.Zarankiewicz.biEval_swap line 58
  13. theorem OAI.Zarankiewicz.biBounded_swap line 71
  14. def OAI.Zarankiewicz.boundedSpace line 86
  15. theorem OAI.Zarankiewicz.coefficients_of_mulRoot line 95
  16. theorem OAI.Zarankiewicz.bi_factor_row line 113
  17. theorem OAI.Zarankiewicz.biEval_mulRoot line 123
  18. theorem OAI.Zarankiewicz.bounded_eval_outer line 129