InsertionSlide.lean`

GitHub source file

246 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PolynomialVacuumAlgebra.insertionSlideLeft line 9
def OAI.PolynomialVacuumAlgebra.insertionSlideRight line 15
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_0 line 19
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_1 line 25
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_2 line 30
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_3 line 35
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_4 line 40
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_5 line 45
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_6 line 51
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_7 line 56
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_0_8 line 62
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_0 line 67
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_1 line 72
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_2 line 78
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_3 line 83
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_4 line 89
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_5 line 94
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_6 line 99
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_7 line 104
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_1_8 line 109
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_0 line 114
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_1 line 119
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_2 line 124
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_3 line 130
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_4 line 135
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_5 line 140
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_6 line 145
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_7 line 151
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_2_8 line 156
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_0 line 161
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_1 line 166
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_2 line 172
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_3 line 177
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_4 line 183
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_5 line 188
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_6 line 193
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_7 line 198
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_3_8 line 203
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_0 line 208
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_1 line 213
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_2 line 218
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_3 line 223
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_4 line 228
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_5 line 234
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_6 line 239
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_7 line 244
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_4_8 line 249
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_0 line 254
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_1 line 260
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_2 line 265
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_3 line 270
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_4 line 275
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_5 line 280
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_6 line 286
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_7 line 291
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_5_8 line 297
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_0 line 302
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_1 line 307
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_2 line 312
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_3 line 318
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_4 line 323
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_5 line 328
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_6 line 333
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_7 line 339
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_6_8 line 344
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_0 line 349
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_1 line 355
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_2 line 360
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_3 line 365
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_4 line 370
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_5 line 375
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_6 line 381
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_7 line 386
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_7_8 line 392
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_0 line 397
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_1 line 402
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_2 line 407
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_3 line 412
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_4 line 417
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_5 line 422
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_6 line 427
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_7 line 432
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_8_8 line 437
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_0 line 443
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_1 line 448
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_2 line 454
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_3 line 459
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_4 line 465
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_5 line 470
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_6 line 475
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_7 line 480
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_9_8 line 485
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_0 line 490
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_1 line 495
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_2 line 500
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_3 line 505
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_4 line 510
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_5 line 516
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_6 line 521
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_7 line 526
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_10_8 line 531
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_0 line 536
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_1 line 542
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_2 line 547
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_3 line 552
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_4 line 557
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_5 line 562
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_6 line 568
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_7 line 573
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_11_8 line 579
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_0 line 584
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_1 line 589
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_2 line 594
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_3 line 599
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_4 line 604
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_5 line 610
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_6 line 615
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_7 line 620
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_12_8 line 625
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_0 line 630
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_1 line 635
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_2 line 640
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_3 line 645
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_4 line 650
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_5 line 655
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_6 line 660
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_7 line 665
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_13_8 line 670
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_0 line 675
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_1 line 680
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_2 line 686
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_3 line 691
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_4 line 697
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_5 line 702
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_6 line 707
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_7 line 712
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_14_8 line 717
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_0 line 722
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_1 line 728
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_2 line 733
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_3 line 738
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_4 line 743
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_5 line 748
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_6 line 754
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_7 line 759
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_15_8 line 765
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_0 line 770
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_1 line 775
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_2 line 781
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_3 line 786
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_4 line 792
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_5 line 797
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_6 line 802
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_7 line 807
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_16_8 line 812
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_0 line 817
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_1 line 822
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_2 line 827
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_3 line 833
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_4 line 838
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_5 line 843
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_6 line 848
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_7 line 854
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_17_8 line 859
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_0 line 864
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_1 line 869
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_2 line 874
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_3 line 880
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_4 line 885
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_5 line 890
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_6 line 895
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_7 line 901
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_18_8 line 906
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_0 line 911
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_1 line 917
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_2 line 922
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_3 line 927
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_4 line 932
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_5 line 937
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_6 line 943
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_7 line 948
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_19_8 line 954
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_0 line 959
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_1 line 964
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_2 line 969
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_3 line 974
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_4 line 979
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_5 line 984
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_6 line 989
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_7 line 994
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_20_8 line 999
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_0 line 1005
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_1 line 1011
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_2 line 1016
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_3 line 1021
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_4 line 1026
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_5 line 1031
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_6 line 1037
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_7 line 1042
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_21_8 line 1048
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_0 line 1053
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_1 line 1058
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_2 line 1064
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_3 line 1069
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_4 line 1075
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_5 line 1080
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_6 line 1085
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_7 line 1090
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_22_8 line 1095
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_0 line 1100
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_1 line 1105
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_2 line 1110
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_3 line 1116
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_4 line 1121
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_5 line 1126
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_6 line 1131
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_7 line 1137
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_23_8 line 1142
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_0 line 1147
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_1 line 1152
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_2 line 1157
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_3 line 1162
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_4 line 1167
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_5 line 1172
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_6 line 1177
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_7 line 1182
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_24_8 line 1187
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_0 line 1193
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_1 line 1198
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_2 line 1203
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_3 line 1209
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_4 line 1214
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_5 line 1219
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_6 line 1224
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_7 line 1230
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_25_8 line 1235
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_0 line 1240
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_1 line 1245
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_2 line 1250
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_3 line 1255
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_4 line 1260
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_5 line 1265
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_6 line 1270
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_7 line 1275
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_entry_26_8 line 1280
theorem OAI.PolynomialVacuumAlgebra.insertion_slide_coefficients line 1285