OAI/Combinatorics/PolynomialVacuum/Algebra/CupSlide.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumAlgebra.insertionTable line 7
2. theorem OAI.PolynomialVacuumAlgebra.insertion_eq_table line 17
3. def OAI.PolynomialVacuumAlgebra.cupSlideLeft line 26
4. def OAI.PolynomialVacuumAlgebra.cupSlideRight line 31
5. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_0_0 line 35
6. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_0_1 line 43
7. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_0_2 line 48
8. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_1_0 line 53
9. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_1_1 line 58
10. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_1_2 line 66
11. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_2_0 line 71
12. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_2_1 line 76
13. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_2_2 line 81
14. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_3_0 line 89
15. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_3_1 line 94
16. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_3_2 line 102
17. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_4_0 line 107
18. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_4_1 line 112
19. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_4_2 line 117
20. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_5_0 line 122
21. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_5_1 line 130
22. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_5_2 line 135
23. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_6_0 line 140
24. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_6_1 line 145
25. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_6_2 line 150
26. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_7_0 line 158
27. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_7_1 line 166
28. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_7_2 line 171
29. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_8_0 line 176
30. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_8_1 line 181
31. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_8_2 line 186
32. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_9_0 line 191
33. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_9_1 line 196
34. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_9_2 line 204
35. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_10_0 line 209
36. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_10_1 line 214
37. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_10_2 line 219
38. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_11_0 line 224
39. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_11_1 line 232
40. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_11_2 line 237
41. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_12_0 line 242
42. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_12_1 line 247
43. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_12_2 line 252
44. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_13_0 line 257
45. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_13_1 line 262
46. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_13_2 line 267
47. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_14_0 line 272
48. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_14_1 line 277
49. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_14_2 line 286
50. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_15_0 line 291
51. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_15_1 line 299
52. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_15_2 line 304
53. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_16_0 line 309
54. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_16_1 line 314
55. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_16_2 line 322
56. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_17_0 line 327
57. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_17_1 line 332
58. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_17_2 line 337
59. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_18_0 line 345
60. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_18_1 line 350
61. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_18_2 line 355
62. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_19_0 line 363
63. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_19_1 line 371
64. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_19_2 line 376
65. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_20_0 line 381
66. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_20_1 line 386
67. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_20_2 line 391
68. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_21_0 line 396
69. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_21_1 line 404
70. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_21_2 line 409
71. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_22_0 line 414
72. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_22_1 line 419
73. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_22_2 line 427
74. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_23_0 line 432
75. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_23_1 line 437
76. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_23_2 line 442
77. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_24_0 line 450
78. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_24_1 line 455
79. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_24_2 line 460
80. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_25_0 line 465
81. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_25_1 line 470
82. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_25_2 line 475
83. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_26_0 line 484
84. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_26_1 line 489
85. theorem OAI.PolynomialVacuumAlgebra.cup_slide_entry_26_2 line 494
86. theorem OAI.PolynomialVacuumAlgebra.cup_slide_coefficients line 499