OAI/Combinatorics/CompleteCrossing/TriangleFactors.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Triangular evaluation indices, division, and determinant factorization.

  1. def OAI.Paper170.triangleMiddleEmbedding line 15
  2. def OAI.Paper170.triangleEndEmbedding line 18
  3. theorem OAI.Paper170.triangleMiddleEmbedding_strictMono line 21
  4. theorem OAI.Paper170.triangleEndEmbedding_strictMono line 29
  5. theorem OAI.Paper170.triangleMiddleEmbedding_avoids line 35
  6. theorem OAI.Paper170.triangleEndEmbedding_avoids line 41
  7. theorem OAI.Paper170.evenTriangle_delete_middle line 47
  8. theorem OAI.Paper170.evenTriangle_delete_ends line 53
  9. theorem OAI.Paper170.evenTriangle_middle_left_row line 59
  10. theorem OAI.Paper170.evenTriangle_middle_right_row line 64
  11. theorem OAI.Paper170.evenTriangle_first_column line 69
  12. theorem OAI.Paper170.evenTriangle_last_column line 74
  13. theorem OAI.Paper170.triangleMiddleEmbedding_range line 79
  14. theorem OAI.Paper170.triangleEndEmbedding_range line 94
  15. theorem OAI.Paper170.evenTriangle_middle_left_card line 105
  16. theorem OAI.Paper170.evenTriangle_middle_right_card line 114
  17. theorem OAI.Paper170.evenTriangle_first_column_card line 125
  18. theorem OAI.Paper170.evenTriangle_last_column_card line 135
  19. theorem OAI.Paper170.evenTriangle_two line 146
  20. theorem OAI.Paper170.evenTriangle_two_distinct_coordinates line 150
  21. theorem OAI.Paper170.mem_rectangle_of_toBiPolynomial_bounded line 166
  22. theorem OAI.Paper170.bi_factor_two_rows line 190
  23. theorem OAI.Paper170.evenTriangle_middle_rows_zero line 201
  24. theorem OAI.Paper170.evenTriangle_end_columns_zero line 232
  25. theorem OAI.Paper170.evalTwo_ext line 283
  26. theorem OAI.Paper170.evenTriangle_row_factorization line 290
  27. theorem OAI.Paper170.evenTriangle_column_factorization line 339