OAI/Combinatorics/PolynomialVacuum/Algebra/BaseThree.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_0 line 8
2. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_0 line 17
3. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_0 line 25
4. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_1 line 33
5. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_1 line 41
6. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_1 line 48
7. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_2 line 55
8. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_2 line 63
9. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_2 line 70
10. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_3 line 77
11. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_3 line 85
12. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_3 line 92
13. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_4 line 99
14. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_4 line 107
15. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_4 line 114
16. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_5 line 121
17. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_5 line 130
18. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_5 line 137
19. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_6 line 145
20. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_6 line 153
21. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_6 line 160
22. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_7 line 167
23. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_7 line 176
24. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_7 line 183
25. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_8 line 191
26. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_8 line 199
27. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_8 line 206
28. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_9 line 213
29. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_9 line 221
30. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_9 line 228
31. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_10 line 235
32. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_10 line 243
33. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_10 line 250
34. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_11 line 257
35. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_11 line 266
36. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_11 line 274
37. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_12 line 282
38. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_12 line 290
39. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_12 line 297
40. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_13 line 304
41. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_13 line 312
42. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_13 line 319
43. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_14 line 326
44. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_14 line 334
45. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_14 line 341
46. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_15 line 348
47. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_15 line 357
48. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_15 line 365
49. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_16 line 373
50. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_16 line 381
51. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_16 line 388
52. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_17 line 395
53. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_17 line 403
54. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_17 line 410
55. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_18 line 417
56. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_18 line 425
57. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_18 line 432
58. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_19 line 439
59. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_19 line 448
60. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_19 line 456
61. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_20 line 464
62. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_20 line 472
63. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_20 line 479
64. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_21 line 486
65. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_21 line 495
66. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_21 line 503
67. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_22 line 511
68. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_22 line 519
69. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_22 line 526
70. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_23 line 533
71. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_23 line 541
72. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_23 line 548
73. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_24 line 555
74. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_24 line 563
75. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_24 line 570
76. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_25 line 577
77. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_25 line 585
78. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_25 line 592
79. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange_26 line 599
80. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation_26 line 607
81. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup_26 line 614
82. theorem OAI.PolynomialVacuumAlgebra.baseThree_exchange line 621
83. theorem OAI.PolynomialVacuumAlgebra.baseThree_rotation line 653
84. theorem OAI.PolynomialVacuumAlgebra.baseThree_cup line 685