OAI/Analysis/LaughlinGap/SumTable21.lean

GitHub source file

178 declarations, 0 contain sorry, 0 declared as axioms

Sum Table21.

  1. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_0 line 16
  2. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_0_checked line 17
  3. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_1 line 21
  4. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_1_checked line 22
  5. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_2 line 26
  6. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_2_checked line 27
  7. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_3 line 31
  8. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_3_checked line 32
  9. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_4 line 36
  10. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_4_checked line 37
  11. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_5 line 41
  12. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_5_checked line 42
  13. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_6 line 46
  14. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_6_checked line 47
  15. def OAI.LaughlinGap.RealOccupation.SumTable21.s_0_7 line 51
  16. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_0_7_checked line 52
  17. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_0 line 56
  18. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_0_checked line 57
  19. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_1 line 61
  20. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_1_checked line 62
  21. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_2 line 66
  22. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_2_checked line 67
  23. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_3 line 71
  24. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_3_checked line 72
  25. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_4 line 76
  26. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_4_checked line 77
  27. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_5 line 81
  28. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_5_checked line 82
  29. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_6 line 86
  30. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_6_checked line 87
  31. def OAI.LaughlinGap.RealOccupation.SumTable21.s_1_7 line 91
  32. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_1_7_checked line 92
  33. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_0 line 96
  34. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_0_checked line 97
  35. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_1 line 101
  36. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_1_checked line 102
  37. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_2 line 106
  38. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_2_checked line 107
  39. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_3 line 111
  40. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_3_checked line 112
  41. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_4 line 116
  42. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_4_checked line 117
  43. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_5 line 121
  44. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_5_checked line 122
  45. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_6 line 126
  46. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_6_checked line 127
  47. def OAI.LaughlinGap.RealOccupation.SumTable21.s_2_7 line 131
  48. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_2_7_checked line 132
  49. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_0 line 136
  50. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_0_checked line 137
  51. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_1 line 141
  52. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_1_checked line 142
  53. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_2 line 146
  54. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_2_checked line 147
  55. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_3 line 151
  56. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_3_checked line 152
  57. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_4 line 156
  58. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_4_checked line 157
  59. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_5 line 161
  60. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_5_checked line 162
  61. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_6 line 166
  62. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_6_checked line 167
  63. def OAI.LaughlinGap.RealOccupation.SumTable21.s_3_7 line 171
  64. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_3_7_checked line 172
  65. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_0 line 176
  66. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_0_checked line 177
  67. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_1 line 181
  68. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_1_checked line 182
  69. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_2 line 186
  70. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_2_checked line 187
  71. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_3 line 191
  72. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_3_checked line 192
  73. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_4 line 196
  74. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_4_checked line 197
  75. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_5 line 201
  76. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_5_checked line 202
  77. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_6 line 206
  78. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_6_checked line 207
  79. def OAI.LaughlinGap.RealOccupation.SumTable21.s_4_7 line 211
  80. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_4_7_checked line 212
  81. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_0 line 216
  82. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_0_checked line 217
  83. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_1 line 221
  84. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_1_checked line 222
  85. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_2 line 226
  86. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_2_checked line 227
  87. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_3 line 231
  88. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_3_checked line 232
  89. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_4 line 236
  90. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_4_checked line 237
  91. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_5 line 241
  92. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_5_checked line 242
  93. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_6 line 246
  94. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_6_checked line 247
  95. def OAI.LaughlinGap.RealOccupation.SumTable21.s_5_7 line 251
  96. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_5_7_checked line 252
  97. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_0 line 256
  98. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_0_checked line 257
  99. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_1 line 261
  100. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_1_checked line 262
  101. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_2 line 266
  102. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_2_checked line 267
  103. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_3 line 271
  104. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_3_checked line 272
  105. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_4 line 276
  106. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_4_checked line 277
  107. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_5 line 281
  108. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_5_checked line 282
  109. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_6 line 286
  110. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_6_checked line 287
  111. def OAI.LaughlinGap.RealOccupation.SumTable21.s_6_7 line 291
  112. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_6_7_checked line 292
  113. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_0 line 296
  114. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_0_checked line 297
  115. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_1 line 301
  116. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_1_checked line 302
  117. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_2 line 306
  118. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_2_checked line 307
  119. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_3 line 311
  120. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_3_checked line 312
  121. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_4 line 316
  122. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_4_checked line 317
  123. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_5 line 321
  124. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_5_checked line 322
  125. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_6 line 326
  126. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_6_checked line 327
  127. def OAI.LaughlinGap.RealOccupation.SumTable21.s_7_7 line 331
  128. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_7_7_checked line 332
  129. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_0 line 336
  130. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_0_checked line 337
  131. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_1 line 341
  132. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_1_checked line 342
  133. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_2 line 346
  134. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_2_checked line 347
  135. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_3 line 351
  136. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_3_checked line 352
  137. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_4 line 356
  138. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_4_checked line 357
  139. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_5 line 361
  140. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_5_checked line 362
  141. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_6 line 366
  142. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_6_checked line 367
  143. def OAI.LaughlinGap.RealOccupation.SumTable21.s_8_7 line 371
  144. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_8_7_checked line 372
  145. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_0 line 376
  146. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_0_checked line 377
  147. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_1 line 381
  148. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_1_checked line 382
  149. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_2 line 386
  150. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_2_checked line 387
  151. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_3 line 391
  152. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_3_checked line 392
  153. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_4 line 396
  154. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_4_checked line 397
  155. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_5 line 401
  156. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_5_checked line 402
  157. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_6 line 406
  158. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_6_checked line 407
  159. def OAI.LaughlinGap.RealOccupation.SumTable21.s_9_7 line 411
  160. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_9_7_checked line 412
  161. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_0 line 416
  162. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_0_checked line 417
  163. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_1 line 421
  164. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_1_checked line 422
  165. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_2 line 426
  166. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_2_checked line 427
  167. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_3 line 431
  168. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_3_checked line 432
  169. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_4 line 436
  170. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_4_checked line 437
  171. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_5 line 441
  172. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_5_checked line 442
  173. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_6 line 446
  174. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_6_checked line 447
  175. def OAI.LaughlinGap.RealOccupation.SumTable21.s_10_7 line 451
  176. lemma OAI.LaughlinGap.RealOccupation.SumTable21.s_10_7_checked line 452
  177. def OAI.LaughlinGap.RealOccupation.SumTable21.sums line 456
  178. lemma OAI.LaughlinGap.RealOccupation.SumTable21.sums_checked line 457