OAI/Combinatorics/CompleteCrossing/Isotropy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Isotropic evaluation image and order-pairing identities.

  1. theorem OAI.Paper170.evalFour_swap_first line 15
  2. theorem OAI.Paper170.evalFour_swap_second line 23
  3. theorem OAI.Paper170.evalFour_fullDifference line 31
  4. def OAI.Paper170.isotropicTerm line 37
  5. theorem OAI.Paper170.isotropicTerm_first line 44
  6. theorem OAI.Paper170.isotropicTerm_second line 59
  7. theorem OAI.Paper170.isotropicTerm_vanish line 74
  8. theorem OAI.Paper170.support_sum_eq_upper line 81
  9. theorem OAI.Paper170.supportBilinear_eq_isotropicSum line 109
  10. theorem OAI.Paper170.isotropic_test_degree line 126
  11. theorem OAI.Paper170.polynomialTest_isotropic line 139
  12. theorem OAI.Paper170.evaluation_image_isotropic line 166
  13. theorem OAI.Paper170.weightedPairing_diagonal_invariant line 194
  14. theorem OAI.Paper170.support_swap_mem line 207
  15. def OAI.Paper170.supportEdgeSwap line 215
  16. theorem OAI.Paper170.supportEdgeSwap_involutive line 219
  17. theorem OAI.Paper170.supportEdgeSwap_ne line 223
  18. theorem OAI.Paper170.supportDiagonal_swap line 230
  19. theorem OAI.Paper170.supportBilinear_symmetric line 239
  20. theorem OAI.Paper170.supportDiagonal_swap_block line 247