OAI/Analysis/LaughlinFock/Certificate21Data.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Certificate21 Data.

  1. def OAI.LaughlinFock.fourYData_21 line 14
  2. def OAI.LaughlinFock.fourZData_21 line 29
  3. def OAI.LaughlinFock.fourLData_21 line 44
  4. def OAI.LaughlinFock.fourPivotData_21 line 59
  5. theorem OAI.LaughlinFock.fourOccupations_21 line 62
  6. theorem OAI.LaughlinFock.fourYNumber_21_1_1 line 65
  7. theorem OAI.LaughlinFock.fourYNumber_21_3_1 line 69
  8. theorem OAI.LaughlinFock.fourYNumber_21_3_3 line 73
  9. theorem OAI.LaughlinFock.fourYNumber_21_5_1 line 77
  10. theorem OAI.LaughlinFock.fourYNumber_21_5_3 line 81
  11. theorem OAI.LaughlinFock.fourYNumber_21_5_5 line 85
  12. theorem OAI.LaughlinFock.fourYNumber_21_7_1 line 89
  13. theorem OAI.LaughlinFock.fourYNumber_21_7_3 line 93
  14. theorem OAI.LaughlinFock.fourYNumber_21_7_5 line 97
  15. theorem OAI.LaughlinFock.fourYNumber_21_7_7 line 101
  16. theorem OAI.LaughlinFock.fourYNumber_21_9_1 line 105
  17. theorem OAI.LaughlinFock.fourYNumber_21_9_3 line 109
  18. theorem OAI.LaughlinFock.fourYNumber_21_9_5 line 113
  19. theorem OAI.LaughlinFock.fourYNumber_21_9_7 line 117
  20. theorem OAI.LaughlinFock.fourYNumber_21_9_9 line 121
  21. theorem OAI.LaughlinFock.fourYNumber_21_11_1 line 125
  22. theorem OAI.LaughlinFock.fourYNumber_21_11_3 line 129
  23. theorem OAI.LaughlinFock.fourYNumber_21_11_5 line 133
  24. theorem OAI.LaughlinFock.fourYNumber_21_11_7 line 137
  25. theorem OAI.LaughlinFock.fourYNumber_21_11_9 line 141
  26. theorem OAI.LaughlinFock.fourYNumber_21_11_11 line 145
  27. theorem OAI.LaughlinFock.fourYNumber_21_13_1 line 149
  28. theorem OAI.LaughlinFock.fourYNumber_21_13_3 line 153
  29. theorem OAI.LaughlinFock.fourYNumber_21_13_5 line 157
  30. theorem OAI.LaughlinFock.fourYNumber_21_13_7 line 161
  31. theorem OAI.LaughlinFock.fourYNumber_21_13_9 line 165
  32. theorem OAI.LaughlinFock.fourYNumber_21_13_11 line 169
  33. theorem OAI.LaughlinFock.fourYNumber_21_13_13 line 173
  34. theorem OAI.LaughlinFock.fourYNumber_21_15_1 line 177
  35. theorem OAI.LaughlinFock.fourYNumber_21_15_3 line 181
  36. theorem OAI.LaughlinFock.fourYNumber_21_15_5 line 185
  37. theorem OAI.LaughlinFock.fourYNumber_21_15_7 line 189
  38. theorem OAI.LaughlinFock.fourYNumber_21_15_9 line 193
  39. theorem OAI.LaughlinFock.fourYNumber_21_15_11 line 197
  40. theorem OAI.LaughlinFock.fourYNumber_21_15_13 line 201
  41. theorem OAI.LaughlinFock.fourYNumber_21_15_15 line 205
  42. theorem OAI.LaughlinFock.fourYNumber_21_17_1 line 209
  43. theorem OAI.LaughlinFock.fourYNumber_21_17_3 line 213
  44. theorem OAI.LaughlinFock.fourYNumber_21_17_5 line 217
  45. theorem OAI.LaughlinFock.fourYNumber_21_17_7 line 221
  46. theorem OAI.LaughlinFock.fourYNumber_21_17_9 line 225
  47. theorem OAI.LaughlinFock.fourYNumber_21_17_11 line 229
  48. theorem OAI.LaughlinFock.fourYNumber_21_17_13 line 233
  49. theorem OAI.LaughlinFock.fourYNumber_21_17_15 line 237
  50. theorem OAI.LaughlinFock.fourYNumber_21_17_17 line 241
  51. theorem OAI.LaughlinFock.fourYNumber_21_19_1 line 245
  52. theorem OAI.LaughlinFock.fourYNumber_21_19_3 line 249
  53. theorem OAI.LaughlinFock.fourYNumber_21_19_5 line 253
  54. theorem OAI.LaughlinFock.fourYNumber_21_19_7 line 257
  55. theorem OAI.LaughlinFock.fourYNumber_21_19_9 line 261
  56. theorem OAI.LaughlinFock.fourYNumber_21_19_11 line 265
  57. theorem OAI.LaughlinFock.fourYNumber_21_19_13 line 269
  58. theorem OAI.LaughlinFock.fourYNumber_21_19_15 line 273
  59. theorem OAI.LaughlinFock.fourYNumber_21_19_17 line 277
  60. theorem OAI.LaughlinFock.fourYNumber_21_19_19 line 281
  61. theorem OAI.LaughlinFock.fourYNumber_21_21_1 line 285
  62. theorem OAI.LaughlinFock.fourYNumber_21_21_3 line 289
  63. theorem OAI.LaughlinFock.fourYNumber_21_21_5 line 293
  64. theorem OAI.LaughlinFock.fourYNumber_21_21_7 line 297
  65. theorem OAI.LaughlinFock.fourYNumber_21_21_9 line 301
  66. theorem OAI.LaughlinFock.fourYNumber_21_21_11 line 305
  67. theorem OAI.LaughlinFock.fourYNumber_21_21_13 line 309
  68. theorem OAI.LaughlinFock.fourYNumber_21_21_15 line 313
  69. theorem OAI.LaughlinFock.fourYNumber_21_21_17 line 317
  70. theorem OAI.LaughlinFock.fourYNumber_21_21_19 line 321
  71. theorem OAI.LaughlinFock.fourYNumber_21_21_21 line 325