OAI/Combinatorics/Crossing/Interpolation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Zarankiewicz.bounded_sum line 14
  2. theorem OAI.Zarankiewicz.eq_zero_of_node_roots line 24
  3. def OAI.Zarankiewicz.nodeEvaluation line 47
  4. theorem OAI.Zarankiewicz.nodeEvaluation_injective line 53
  5. def OAI.Zarankiewicz.vectorInterpolant line 65
  6. theorem OAI.Zarankiewicz.eval_vectorInterpolant line 70
  7. theorem OAI.Zarankiewicz.bounded_vectorInterpolant line 80
  8. theorem OAI.Zarankiewicz.nodeEvaluation_surjective line 93
  9. def OAI.Zarankiewicz.nodeEvaluationEquiv line 105
  10. theorem OAI.Zarankiewicz.finrank_constrained_zero line 110
  11. theorem OAI.Zarankiewicz.constrained_finrank_mono line 121
  12. theorem OAI.Zarankiewicz.sum_rankIncrement line 129
  13. theorem OAI.Zarankiewicz.interpolation_identity line 136