OAI/Combinatorics/Crossing/PolynomialKernel.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.Bounded line 14
  2. theorem OAI.Zarankiewicz.bounded_zero line 17
  3. theorem OAI.Zarankiewicz.bounded_mono line 21
  4. theorem OAI.Zarankiewicz.bounded_add line 25
  5. theorem OAI.Zarankiewicz.bounded_sub line 30
  6. theorem OAI.Zarankiewicz.bounded_single line 36
  7. theorem OAI.Zarankiewicz.bounded_zero_iff line 41
  8. def OAI.Zarankiewicz.mulRoot line 49
  9. theorem OAI.Zarankiewicz.mulRoot_coeff_zero line 52
  10. theorem OAI.Zarankiewicz.mulRoot_coeff_succ line 60
  11. theorem OAI.Zarankiewicz.eval_mulRoot line 68
  12. theorem OAI.Zarankiewicz.bounded_mulRoot line 72
  13. theorem OAI.Zarankiewicz.eq_constant_of_bounded_one line 79
  14. theorem OAI.Zarankiewicz.exists_mulRoot_of_eval_zero line 86
  15. theorem OAI.Zarankiewicz.eq_zero_of_mulRoot_eq_zero line 118
  16. def OAI.Zarankiewicz.mulRootLinear line 133
  17. def OAI.Zarankiewicz.constrained line 140
  18. def OAI.Zarankiewicz.constrainedEval line 160
  19. def OAI.Zarankiewicz.toEvalKernel line 163
  20. theorem OAI.Zarankiewicz.toEvalKernel_injective line 180
  21. theorem OAI.Zarankiewicz.toEvalKernel_surjective line 192
  22. def OAI.Zarankiewicz.evalKernelEquiv line 206
  23. def OAI.Zarankiewicz.constrainedCoefficients line 211
  24. theorem OAI.Zarankiewicz.constrainedCoefficients_injective line 216
  25. instance OAI.Zarankiewicz.constrained_finiteDimensional line 227
  26. def OAI.Zarankiewicz.rankIncrement line 232
  27. theorem OAI.Zarankiewicz.finrank_eval_range line 235