OAI/Combinatorics/Hamiltonian/PairPolynomials.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

First nonzero coefficients of paired-state polynomials.

  1. theorem OAI.Barnette.common_phase_sum_ne_zero line 12
  2. def OAI.Barnette.linearProduct line 51
  3. theorem OAI.Barnette.linearProduct_coeff_zero line 54
  4. theorem OAI.Barnette.linearProduct_coeff_one line 58
  5. theorem OAI.Barnette.cycle_difference_divX_coeff_zero line 69
  6. theorem OAI.Barnette.cycle_difference_eq_X_mul_divX line 75
  7. theorem OAI.Barnette.cycle_group_polynomials_ne_zero line 82
  8. theorem OAI.Barnette.phase_sum line 106
  9. theorem OAI.Barnette.phase_three line 118
  10. theorem OAI.Barnette.phase_neg_three line 119
  11. theorem OAI.Barnette.phase_neg_of_disk line 121
  12. def OAI.Barnette.TriangleSystem.Pair.cycleFaces line 128
  13. theorem OAI.Barnette.TriangleSystem.Pair.mem_cycleFaces line 132
  14. def OAI.Barnette.TriangleSystem.Pair.cycleDelta line 137
  15. theorem OAI.Barnette.TriangleSystem.Pair.orient_left_val line 141
  16. theorem OAI.Barnette.TriangleSystem.Pair.orient_right_val line 146
  17. theorem OAI.Barnette.TriangleSystem.Pair.orient_delta_sum line 150
  18. theorem OAI.Barnette.TriangleSystem.Pair.orient_rawIndexSum line 169
  19. theorem OAI.Barnette.TriangleSystem.Pair.orient_phase line 179
  20. def OAI.Barnette.TriangleSystem.Pair.stateWeight line 192
  21. def OAI.Barnette.TriangleSystem.Pair.cycleLeftWeight line 195
  22. def OAI.Barnette.TriangleSystem.Pair.cycleRightWeight line 199
  23. theorem OAI.Barnette.TriangleSystem.Pair.orient_weight line 203
  24. def OAI.Barnette.TriangleSystem.Pair.term line 224
  25. theorem OAI.Barnette.TriangleSystem.Pair.orient_term line 227
  26. theorem OAI.Barnette.TriangleSystem.Pair.group_sum_product line 238
  27. def OAI.Barnette.TriangleSystem.Pair.cycleSlope line 276
  28. theorem OAI.Barnette.TriangleSystem.Pair.cycle_diff_coeff_one line 281
  29. theorem OAI.Barnette.TriangleSystem.Pair.cycle_factor_witness line 288
  30. def OAI.Barnette.TriangleSystem.Pair.GroupIndex line 313
  31. instance OAI.Barnette.TriangleSystem.Pair.(instance at line 315) line 315
  32. def OAI.Barnette.TriangleSystem.Pair.GroupIndex.representative line 318
  33. theorem OAI.Barnette.TriangleSystem.Pair.GroupIndex.representative_third line 322
  34. def OAI.Barnette.TriangleSystem.Pair.groupIndex line 325
  35. def OAI.Barnette.TriangleSystem.Pair.GroupIndex.fiberEquivGroup line 327
  36. theorem OAI.Barnette.TriangleSystem.Pair.sum_groups line 339
  37. theorem OAI.Barnette.TriangleSystem.Pair.total_sum_ne_zero line 348
  38. def OAI.Barnette.TriangleSystem.Pair.secondFiberEquiv line 397
  39. theorem OAI.Barnette.TriangleSystem.Pair.sum_second_states line 409
  40. theorem OAI.Barnette.TriangleSystem.Pair.forest_pair_of_disk_circulation line 423