OAI/Analysis/LaughlinGap/SumTable20.lean

GitHub source file

162 declarations, 0 contain sorry, 0 declared as axioms

Sum Table20.

  1. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_0 line 15
  2. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_0_checked line 16
  3. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_1 line 20
  4. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_1_checked line 21
  5. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_2 line 25
  6. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_2_checked line 26
  7. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_3 line 30
  8. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_3_checked line 31
  9. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_4 line 35
  10. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_4_checked line 36
  11. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_5 line 40
  12. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_5_checked line 41
  13. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_6 line 45
  14. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_6_checked line 46
  15. def OAI.LaughlinGap.RealOccupation.SumTable20.s_0_7 line 50
  16. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_0_7_checked line 51
  17. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_0 line 55
  18. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_0_checked line 56
  19. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_1 line 60
  20. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_1_checked line 61
  21. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_2 line 65
  22. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_2_checked line 66
  23. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_3 line 70
  24. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_3_checked line 71
  25. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_4 line 75
  26. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_4_checked line 76
  27. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_5 line 80
  28. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_5_checked line 81
  29. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_6 line 85
  30. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_6_checked line 86
  31. def OAI.LaughlinGap.RealOccupation.SumTable20.s_1_7 line 90
  32. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_1_7_checked line 91
  33. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_0 line 95
  34. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_0_checked line 96
  35. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_1 line 100
  36. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_1_checked line 101
  37. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_2 line 105
  38. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_2_checked line 106
  39. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_3 line 110
  40. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_3_checked line 111
  41. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_4 line 115
  42. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_4_checked line 116
  43. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_5 line 120
  44. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_5_checked line 121
  45. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_6 line 125
  46. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_6_checked line 126
  47. def OAI.LaughlinGap.RealOccupation.SumTable20.s_2_7 line 130
  48. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_2_7_checked line 131
  49. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_0 line 135
  50. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_0_checked line 136
  51. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_1 line 140
  52. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_1_checked line 141
  53. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_2 line 145
  54. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_2_checked line 146
  55. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_3 line 150
  56. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_3_checked line 151
  57. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_4 line 155
  58. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_4_checked line 156
  59. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_5 line 160
  60. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_5_checked line 161
  61. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_6 line 165
  62. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_6_checked line 166
  63. def OAI.LaughlinGap.RealOccupation.SumTable20.s_3_7 line 170
  64. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_3_7_checked line 171
  65. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_0 line 175
  66. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_0_checked line 176
  67. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_1 line 180
  68. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_1_checked line 181
  69. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_2 line 185
  70. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_2_checked line 186
  71. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_3 line 190
  72. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_3_checked line 191
  73. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_4 line 195
  74. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_4_checked line 196
  75. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_5 line 200
  76. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_5_checked line 201
  77. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_6 line 205
  78. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_6_checked line 206
  79. def OAI.LaughlinGap.RealOccupation.SumTable20.s_4_7 line 210
  80. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_4_7_checked line 211
  81. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_0 line 215
  82. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_0_checked line 216
  83. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_1 line 220
  84. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_1_checked line 221
  85. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_2 line 225
  86. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_2_checked line 226
  87. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_3 line 230
  88. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_3_checked line 231
  89. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_4 line 235
  90. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_4_checked line 236
  91. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_5 line 240
  92. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_5_checked line 241
  93. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_6 line 245
  94. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_6_checked line 246
  95. def OAI.LaughlinGap.RealOccupation.SumTable20.s_5_7 line 250
  96. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_5_7_checked line 251
  97. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_0 line 255
  98. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_0_checked line 256
  99. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_1 line 260
  100. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_1_checked line 261
  101. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_2 line 265
  102. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_2_checked line 266
  103. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_3 line 270
  104. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_3_checked line 271
  105. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_4 line 275
  106. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_4_checked line 276
  107. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_5 line 280
  108. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_5_checked line 281
  109. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_6 line 285
  110. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_6_checked line 286
  111. def OAI.LaughlinGap.RealOccupation.SumTable20.s_6_7 line 290
  112. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_6_7_checked line 291
  113. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_0 line 295
  114. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_0_checked line 296
  115. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_1 line 300
  116. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_1_checked line 301
  117. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_2 line 305
  118. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_2_checked line 306
  119. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_3 line 310
  120. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_3_checked line 311
  121. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_4 line 315
  122. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_4_checked line 316
  123. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_5 line 320
  124. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_5_checked line 321
  125. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_6 line 325
  126. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_6_checked line 326
  127. def OAI.LaughlinGap.RealOccupation.SumTable20.s_7_7 line 330
  128. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_7_7_checked line 331
  129. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_0 line 335
  130. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_0_checked line 336
  131. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_1 line 340
  132. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_1_checked line 341
  133. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_2 line 345
  134. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_2_checked line 346
  135. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_3 line 350
  136. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_3_checked line 351
  137. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_4 line 355
  138. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_4_checked line 356
  139. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_5 line 360
  140. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_5_checked line 361
  141. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_6 line 365
  142. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_6_checked line 366
  143. def OAI.LaughlinGap.RealOccupation.SumTable20.s_8_7 line 370
  144. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_8_7_checked line 371
  145. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_0 line 375
  146. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_0_checked line 376
  147. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_1 line 380
  148. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_1_checked line 381
  149. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_2 line 385
  150. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_2_checked line 386
  151. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_3 line 390
  152. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_3_checked line 391
  153. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_4 line 395
  154. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_4_checked line 396
  155. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_5 line 400
  156. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_5_checked line 401
  157. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_6 line 405
  158. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_6_checked line 406
  159. def OAI.LaughlinGap.RealOccupation.SumTable20.s_9_7 line 410
  160. lemma OAI.LaughlinGap.RealOccupation.SumTable20.s_9_7_checked line 411
  161. def OAI.LaughlinGap.RealOccupation.SumTable20.sums line 415
  162. lemma OAI.LaughlinGap.RealOccupation.SumTable20.sums_checked line 416