OAI/Analysis/LaughlinFock/Certificate23Data.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Certificate23 Data.

  1. def OAI.LaughlinFock.fourYData_23 line 14
  2. def OAI.LaughlinFock.fourZData_23 line 30
  3. def OAI.LaughlinFock.fourLData_23 line 46
  4. def OAI.LaughlinFock.fourPivotData_23 line 62
  5. theorem OAI.LaughlinFock.fourOccupations_23 line 65
  6. theorem OAI.LaughlinFock.fourYNumber_23_1_1 line 68
  7. theorem OAI.LaughlinFock.fourYNumber_23_3_1 line 72
  8. theorem OAI.LaughlinFock.fourYNumber_23_3_3 line 76
  9. theorem OAI.LaughlinFock.fourYNumber_23_5_1 line 80
  10. theorem OAI.LaughlinFock.fourYNumber_23_5_3 line 84
  11. theorem OAI.LaughlinFock.fourYNumber_23_5_5 line 88
  12. theorem OAI.LaughlinFock.fourYNumber_23_7_1 line 92
  13. theorem OAI.LaughlinFock.fourYNumber_23_7_3 line 96
  14. theorem OAI.LaughlinFock.fourYNumber_23_7_5 line 100
  15. theorem OAI.LaughlinFock.fourYNumber_23_7_7 line 104
  16. theorem OAI.LaughlinFock.fourYNumber_23_9_1 line 108
  17. theorem OAI.LaughlinFock.fourYNumber_23_9_3 line 112
  18. theorem OAI.LaughlinFock.fourYNumber_23_9_5 line 116
  19. theorem OAI.LaughlinFock.fourYNumber_23_9_7 line 120
  20. theorem OAI.LaughlinFock.fourYNumber_23_9_9 line 124
  21. theorem OAI.LaughlinFock.fourYNumber_23_11_1 line 128
  22. theorem OAI.LaughlinFock.fourYNumber_23_11_3 line 132
  23. theorem OAI.LaughlinFock.fourYNumber_23_11_5 line 136
  24. theorem OAI.LaughlinFock.fourYNumber_23_11_7 line 140
  25. theorem OAI.LaughlinFock.fourYNumber_23_11_9 line 144
  26. theorem OAI.LaughlinFock.fourYNumber_23_11_11 line 148
  27. theorem OAI.LaughlinFock.fourYNumber_23_13_1 line 152
  28. theorem OAI.LaughlinFock.fourYNumber_23_13_3 line 156
  29. theorem OAI.LaughlinFock.fourYNumber_23_13_5 line 160
  30. theorem OAI.LaughlinFock.fourYNumber_23_13_7 line 164
  31. theorem OAI.LaughlinFock.fourYNumber_23_13_9 line 168
  32. theorem OAI.LaughlinFock.fourYNumber_23_13_11 line 172
  33. theorem OAI.LaughlinFock.fourYNumber_23_13_13 line 176
  34. theorem OAI.LaughlinFock.fourYNumber_23_15_1 line 180
  35. theorem OAI.LaughlinFock.fourYNumber_23_15_3 line 184
  36. theorem OAI.LaughlinFock.fourYNumber_23_15_5 line 188
  37. theorem OAI.LaughlinFock.fourYNumber_23_15_7 line 192
  38. theorem OAI.LaughlinFock.fourYNumber_23_15_9 line 196
  39. theorem OAI.LaughlinFock.fourYNumber_23_15_11 line 200
  40. theorem OAI.LaughlinFock.fourYNumber_23_15_13 line 204
  41. theorem OAI.LaughlinFock.fourYNumber_23_15_15 line 208
  42. theorem OAI.LaughlinFock.fourYNumber_23_17_1 line 212
  43. theorem OAI.LaughlinFock.fourYNumber_23_17_3 line 216
  44. theorem OAI.LaughlinFock.fourYNumber_23_17_5 line 220
  45. theorem OAI.LaughlinFock.fourYNumber_23_17_7 line 224
  46. theorem OAI.LaughlinFock.fourYNumber_23_17_9 line 228
  47. theorem OAI.LaughlinFock.fourYNumber_23_17_11 line 232
  48. theorem OAI.LaughlinFock.fourYNumber_23_17_13 line 236
  49. theorem OAI.LaughlinFock.fourYNumber_23_17_15 line 240
  50. theorem OAI.LaughlinFock.fourYNumber_23_17_17 line 244
  51. theorem OAI.LaughlinFock.fourYNumber_23_19_1 line 248
  52. theorem OAI.LaughlinFock.fourYNumber_23_19_3 line 252
  53. theorem OAI.LaughlinFock.fourYNumber_23_19_5 line 256
  54. theorem OAI.LaughlinFock.fourYNumber_23_19_7 line 260
  55. theorem OAI.LaughlinFock.fourYNumber_23_19_9 line 264
  56. theorem OAI.LaughlinFock.fourYNumber_23_19_11 line 268
  57. theorem OAI.LaughlinFock.fourYNumber_23_19_13 line 272
  58. theorem OAI.LaughlinFock.fourYNumber_23_19_15 line 276
  59. theorem OAI.LaughlinFock.fourYNumber_23_19_17 line 280
  60. theorem OAI.LaughlinFock.fourYNumber_23_19_19 line 284
  61. theorem OAI.LaughlinFock.fourYNumber_23_21_1 line 288
  62. theorem OAI.LaughlinFock.fourYNumber_23_21_3 line 292
  63. theorem OAI.LaughlinFock.fourYNumber_23_21_5 line 296
  64. theorem OAI.LaughlinFock.fourYNumber_23_21_7 line 300
  65. theorem OAI.LaughlinFock.fourYNumber_23_21_9 line 304
  66. theorem OAI.LaughlinFock.fourYNumber_23_21_11 line 308
  67. theorem OAI.LaughlinFock.fourYNumber_23_21_13 line 312
  68. theorem OAI.LaughlinFock.fourYNumber_23_21_15 line 316
  69. theorem OAI.LaughlinFock.fourYNumber_23_21_17 line 320
  70. theorem OAI.LaughlinFock.fourYNumber_23_21_19 line 324
  71. theorem OAI.LaughlinFock.fourYNumber_23_21_21 line 328
  72. theorem OAI.LaughlinFock.fourYNumber_23_23_1 line 332
  73. theorem OAI.LaughlinFock.fourYNumber_23_23_3 line 336
  74. theorem OAI.LaughlinFock.fourYNumber_23_23_5 line 340
  75. theorem OAI.LaughlinFock.fourYNumber_23_23_7 line 344
  76. theorem OAI.LaughlinFock.fourYNumber_23_23_9 line 348
  77. theorem OAI.LaughlinFock.fourYNumber_23_23_11 line 352
  78. theorem OAI.LaughlinFock.fourYNumber_23_23_13 line 356
  79. theorem OAI.LaughlinFock.fourYNumber_23_23_15 line 360
  80. theorem OAI.LaughlinFock.fourYNumber_23_23_17 line 364
  81. theorem OAI.LaughlinFock.fourYNumber_23_23_19 line 368
  82. theorem OAI.LaughlinFock.fourYNumber_23_23_21 line 372
  83. theorem OAI.LaughlinFock.fourYNumber_23_23_23 line 376