SumTable22.lean`

GitHub source file

178 declarations, 0 contain sorry, 0 declared as axioms

Sum Table22.

def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_0 line 15
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_0_checked line 16
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_1 line 20
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_1_checked line 21
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_2 line 25
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_2_checked line 26
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_3 line 30
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_3_checked line 31
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_4 line 35
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_4_checked line 36
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_5 line 40
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_5_checked line 41
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_6 line 45
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_6_checked line 46
def OAI.LaughlinGap.RealOccupation.SumTable22.s_0_7 line 50
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_0_7_checked line 51
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_0 line 55
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_0_checked line 56
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_1 line 60
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_1_checked line 61
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_2 line 65
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_2_checked line 66
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_3 line 70
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_3_checked line 71
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_4 line 75
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_4_checked line 76
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_5 line 80
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_5_checked line 81
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_6 line 85
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_6_checked line 86
def OAI.LaughlinGap.RealOccupation.SumTable22.s_1_7 line 90
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_1_7_checked line 91
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_0 line 95
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_0_checked line 96
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_1 line 100
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_1_checked line 101
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_2 line 105
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_2_checked line 106
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_3 line 110
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_3_checked line 111
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_4 line 115
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_4_checked line 116
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_5 line 120
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_5_checked line 121
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_6 line 125
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_6_checked line 126
def OAI.LaughlinGap.RealOccupation.SumTable22.s_2_7 line 130
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_2_7_checked line 131
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_0 line 135
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_0_checked line 136
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_1 line 140
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_1_checked line 141
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_2 line 145
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_2_checked line 146
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_3 line 150
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_3_checked line 151
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_4 line 155
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_4_checked line 156
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_5 line 160
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_5_checked line 161
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_6 line 165
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_6_checked line 166
def OAI.LaughlinGap.RealOccupation.SumTable22.s_3_7 line 170
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_3_7_checked line 171
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_0 line 175
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_0_checked line 176
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_1 line 180
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_1_checked line 181
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_2 line 185
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_2_checked line 186
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_3 line 190
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_3_checked line 191
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_4 line 195
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_4_checked line 196
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_5 line 200
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_5_checked line 201
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_6 line 205
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_6_checked line 206
def OAI.LaughlinGap.RealOccupation.SumTable22.s_4_7 line 210
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_4_7_checked line 211
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_0 line 215
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_0_checked line 216
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_1 line 220
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_1_checked line 221
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_2 line 225
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_2_checked line 226
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_3 line 230
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_3_checked line 231
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_4 line 235
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_4_checked line 236
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_5 line 240
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_5_checked line 241
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_6 line 245
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_6_checked line 246
def OAI.LaughlinGap.RealOccupation.SumTable22.s_5_7 line 250
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_5_7_checked line 251
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_0 line 255
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_0_checked line 256
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_1 line 260
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_1_checked line 261
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_2 line 265
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_2_checked line 266
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_3 line 270
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_3_checked line 271
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_4 line 275
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_4_checked line 276
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_5 line 280
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_5_checked line 281
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_6 line 285
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_6_checked line 286
def OAI.LaughlinGap.RealOccupation.SumTable22.s_6_7 line 290
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_6_7_checked line 291
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_0 line 295
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_0_checked line 296
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_1 line 300
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_1_checked line 301
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_2 line 305
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_2_checked line 306
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_3 line 310
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_3_checked line 311
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_4 line 315
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_4_checked line 316
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_5 line 320
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_5_checked line 321
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_6 line 325
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_6_checked line 326
def OAI.LaughlinGap.RealOccupation.SumTable22.s_7_7 line 330
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_7_7_checked line 331
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_0 line 335
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_0_checked line 336
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_1 line 340
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_1_checked line 341
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_2 line 345
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_2_checked line 346
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_3 line 350
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_3_checked line 351
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_4 line 355
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_4_checked line 356
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_5 line 360
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_5_checked line 361
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_6 line 365
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_6_checked line 366
def OAI.LaughlinGap.RealOccupation.SumTable22.s_8_7 line 370
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_8_7_checked line 371
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_0 line 375
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_0_checked line 376
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_1 line 380
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_1_checked line 381
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_2 line 385
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_2_checked line 386
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_3 line 390
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_3_checked line 391
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_4 line 395
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_4_checked line 396
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_5 line 400
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_5_checked line 401
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_6 line 405
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_6_checked line 406
def OAI.LaughlinGap.RealOccupation.SumTable22.s_9_7 line 410
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_9_7_checked line 411
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_0 line 415
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_0_checked line 416
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_1 line 420
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_1_checked line 421
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_2 line 425
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_2_checked line 426
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_3 line 430
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_3_checked line 431
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_4 line 435
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_4_checked line 436
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_5 line 440
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_5_checked line 441
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_6 line 445
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_6_checked line 446
def OAI.LaughlinGap.RealOccupation.SumTable22.s_10_7 line 450
lemma OAI.LaughlinGap.RealOccupation.SumTable22.s_10_7_checked line 451
def OAI.LaughlinGap.RealOccupation.SumTable22.sums line 455
lemma OAI.LaughlinGap.RealOccupation.SumTable22.sums_checked line 456