OAI/Combinatorics/CompleteCrossing/Triangle.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Even triangular interpolation and unisolvence.

  1. theorem OAI.Paper170.mem_evenTriangle line 16
  2. def OAI.Paper170.evenTriangleOffDiagEquiv line 21
  3. theorem OAI.Paper170.even_triangle_card line 71
  4. theorem OAI.Paper170.biBounded_mulRoot line 90
  5. theorem OAI.Paper170.insertNode_injective line 102
  6. theorem OAI.Paper170.oddTriangle_unisolvent_fin line 121
  7. theorem OAI.Paper170.evenTriangle_unisolvent_first line 144
  8. theorem OAI.Paper170.evenTriangle_unisolvent_second line 182
  9. theorem OAI.Paper170.evenTriangle_vanish_first line 224
  10. theorem OAI.Paper170.evenTriangle_vanish_second line 236
  11. theorem OAI.Paper170.triangleEvaluation_bijective_of_unisolvent line 248
  12. theorem OAI.Paper170.two_triangle_interpolation line 267