OAI/Combinatorics/PolynomialVacuum/Algebra/HomogeneousCupSlide.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.homogeneousCupLeft line 7
  2. def OAI.PolynomialVacuumAlgebra.homogeneousCupRight line 11
  3. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_0_0 line 14
  4. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_0_1 line 19
  5. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_0_2 line 23
  6. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_1_0 line 27
  7. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_1_1 line 31
  8. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_1_2 line 36
  9. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_2_0 line 40
  10. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_2_1 line 44
  11. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_2_2 line 48
  12. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_3_0 line 53
  13. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_3_1 line 57
  14. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_3_2 line 62
  15. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_4_0 line 66
  16. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_4_1 line 70
  17. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_4_2 line 74
  18. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_5_0 line 78
  19. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_5_1 line 83
  20. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_5_2 line 87
  21. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_6_0 line 91
  22. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_6_1 line 95
  23. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_6_2 line 99
  24. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_7_0 line 104
  25. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_7_1 line 109
  26. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_7_2 line 113
  27. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_8_0 line 117
  28. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_8_1 line 121
  29. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_8_2 line 125
  30. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_9_0 line 129
  31. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_9_1 line 133
  32. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_9_2 line 138
  33. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_10_0 line 142
  34. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_10_1 line 146
  35. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_10_2 line 150
  36. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_11_0 line 154
  37. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_11_1 line 159
  38. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_11_2 line 163
  39. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_12_0 line 167
  40. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_12_1 line 171
  41. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_12_2 line 175
  42. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_13_0 line 179
  43. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_13_1 line 183
  44. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_13_2 line 187
  45. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_14_0 line 191
  46. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_14_1 line 195
  47. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_14_2 line 200
  48. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_15_0 line 204
  49. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_15_1 line 209
  50. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_15_2 line 213
  51. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_16_0 line 217
  52. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_16_1 line 221
  53. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_16_2 line 226
  54. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_17_0 line 230
  55. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_17_1 line 234
  56. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_17_2 line 238
  57. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_18_0 line 243
  58. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_18_1 line 247
  59. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_18_2 line 251
  60. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_19_0 line 256
  61. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_19_1 line 261
  62. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_19_2 line 265
  63. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_20_0 line 269
  64. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_20_1 line 273
  65. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_20_2 line 277
  66. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_21_0 line 281
  67. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_21_1 line 286
  68. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_21_2 line 290
  69. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_22_0 line 294
  70. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_22_1 line 298
  71. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_22_2 line 303
  72. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_23_0 line 307
  73. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_23_1 line 311
  74. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_23_2 line 315
  75. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_24_0 line 320
  76. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_24_1 line 324
  77. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_24_2 line 328
  78. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_25_0 line 332
  79. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_25_1 line 336
  80. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_25_2 line 340
  81. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_26_0 line 345
  82. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_26_1 line 349
  83. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_entry_26_2 line 353
  84. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_slide line 357