OAI/Combinatorics/PolynomialVacuum/Algebra/HomogeneousCupUnslide.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumAlgebra.homogeneousUncupLeft line 7
2. def OAI.PolynomialVacuumAlgebra.homogeneousUncupRight line 10
3. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_0_0 line 13
4. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_0_1 line 18
5. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_0_2 line 22
6. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_1_0 line 26
7. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_1_1 line 30
8. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_1_2 line 35
9. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_2_0 line 39
10. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_2_1 line 43
11. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_2_2 line 47
12. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_3_0 line 52
13. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_3_1 line 56
14. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_3_2 line 61
15. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_4_0 line 65
16. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_4_1 line 69
17. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_4_2 line 73
18. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_5_0 line 77
19. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_5_1 line 82
20. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_5_2 line 86
21. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_6_0 line 90
22. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_6_1 line 94
23. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_6_2 line 98
24. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_7_0 line 103
25. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_7_1 line 108
26. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_7_2 line 112
27. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_8_0 line 116
28. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_8_1 line 120
29. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_8_2 line 124
30. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_9_0 line 128
31. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_9_1 line 132
32. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_9_2 line 137
33. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_10_0 line 141
34. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_10_1 line 145
35. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_10_2 line 149
36. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_11_0 line 153
37. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_11_1 line 158
38. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_11_2 line 162
39. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_12_0 line 166
40. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_12_1 line 170
41. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_12_2 line 174
42. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_13_0 line 178
43. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_13_1 line 182
44. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_13_2 line 186
45. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_14_0 line 190
46. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_14_1 line 194
47. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_14_2 line 199
48. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_15_0 line 203
49. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_15_1 line 208
50. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_15_2 line 212
51. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_16_0 line 216
52. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_16_1 line 220
53. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_16_2 line 225
54. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_17_0 line 229
55. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_17_1 line 233
56. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_17_2 line 237
57. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_18_0 line 242
58. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_18_1 line 246
59. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_18_2 line 250
60. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_19_0 line 255
61. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_19_1 line 260
62. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_19_2 line 264
63. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_20_0 line 268
64. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_20_1 line 272
65. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_20_2 line 276
66. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_21_0 line 280
67. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_21_1 line 285
68. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_21_2 line 289
69. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_22_0 line 293
70. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_22_1 line 297
71. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_22_2 line 302
72. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_23_0 line 306
73. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_23_1 line 310
74. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_23_2 line 314
75. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_24_0 line 319
76. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_24_1 line 323
77. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_24_2 line 327
78. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_25_0 line 331
79. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_25_1 line 335
80. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_25_2 line 339
81. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_26_0 line 344
82. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_26_1 line 348
83. theorem OAI.PolynomialVacuumAlgebra.homogeneous_uncup_entry_26_2 line 352
84. theorem OAI.PolynomialVacuumAlgebra.homogeneous_cup_unslide line 356