OAI/Analysis/LaughlinFock/Certificate20Data.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Certificate20 Data.

  1. def OAI.LaughlinFock.fourYData_20 line 14
  2. def OAI.LaughlinFock.fourZData_20 line 28
  3. def OAI.LaughlinFock.fourLData_20 line 42
  4. def OAI.LaughlinFock.fourPivotData_20 line 56
  5. theorem OAI.LaughlinFock.fourOccupations_20 line 59
  6. theorem OAI.LaughlinFock.fourYNumber_20_1_1 line 62
  7. theorem OAI.LaughlinFock.fourYNumber_20_3_1 line 66
  8. theorem OAI.LaughlinFock.fourYNumber_20_3_3 line 70
  9. theorem OAI.LaughlinFock.fourYNumber_20_5_1 line 74
  10. theorem OAI.LaughlinFock.fourYNumber_20_5_3 line 78
  11. theorem OAI.LaughlinFock.fourYNumber_20_5_5 line 82
  12. theorem OAI.LaughlinFock.fourYNumber_20_7_1 line 86
  13. theorem OAI.LaughlinFock.fourYNumber_20_7_3 line 90
  14. theorem OAI.LaughlinFock.fourYNumber_20_7_5 line 94
  15. theorem OAI.LaughlinFock.fourYNumber_20_7_7 line 98
  16. theorem OAI.LaughlinFock.fourYNumber_20_9_1 line 102
  17. theorem OAI.LaughlinFock.fourYNumber_20_9_3 line 106
  18. theorem OAI.LaughlinFock.fourYNumber_20_9_5 line 110
  19. theorem OAI.LaughlinFock.fourYNumber_20_9_7 line 114
  20. theorem OAI.LaughlinFock.fourYNumber_20_9_9 line 118
  21. theorem OAI.LaughlinFock.fourYNumber_20_11_1 line 122
  22. theorem OAI.LaughlinFock.fourYNumber_20_11_3 line 126
  23. theorem OAI.LaughlinFock.fourYNumber_20_11_5 line 130
  24. theorem OAI.LaughlinFock.fourYNumber_20_11_7 line 134
  25. theorem OAI.LaughlinFock.fourYNumber_20_11_9 line 138
  26. theorem OAI.LaughlinFock.fourYNumber_20_11_11 line 142
  27. theorem OAI.LaughlinFock.fourYNumber_20_13_1 line 146
  28. theorem OAI.LaughlinFock.fourYNumber_20_13_3 line 150
  29. theorem OAI.LaughlinFock.fourYNumber_20_13_5 line 154
  30. theorem OAI.LaughlinFock.fourYNumber_20_13_7 line 158
  31. theorem OAI.LaughlinFock.fourYNumber_20_13_9 line 162
  32. theorem OAI.LaughlinFock.fourYNumber_20_13_11 line 166
  33. theorem OAI.LaughlinFock.fourYNumber_20_13_13 line 170
  34. theorem OAI.LaughlinFock.fourYNumber_20_15_1 line 174
  35. theorem OAI.LaughlinFock.fourYNumber_20_15_3 line 178
  36. theorem OAI.LaughlinFock.fourYNumber_20_15_5 line 182
  37. theorem OAI.LaughlinFock.fourYNumber_20_15_7 line 186
  38. theorem OAI.LaughlinFock.fourYNumber_20_15_9 line 190
  39. theorem OAI.LaughlinFock.fourYNumber_20_15_11 line 194
  40. theorem OAI.LaughlinFock.fourYNumber_20_15_13 line 198
  41. theorem OAI.LaughlinFock.fourYNumber_20_15_15 line 202
  42. theorem OAI.LaughlinFock.fourYNumber_20_17_1 line 206
  43. theorem OAI.LaughlinFock.fourYNumber_20_17_3 line 210
  44. theorem OAI.LaughlinFock.fourYNumber_20_17_5 line 214
  45. theorem OAI.LaughlinFock.fourYNumber_20_17_7 line 218
  46. theorem OAI.LaughlinFock.fourYNumber_20_17_9 line 222
  47. theorem OAI.LaughlinFock.fourYNumber_20_17_11 line 226
  48. theorem OAI.LaughlinFock.fourYNumber_20_17_13 line 230
  49. theorem OAI.LaughlinFock.fourYNumber_20_17_15 line 234
  50. theorem OAI.LaughlinFock.fourYNumber_20_17_17 line 238
  51. theorem OAI.LaughlinFock.fourYNumber_20_19_1 line 242
  52. theorem OAI.LaughlinFock.fourYNumber_20_19_3 line 246
  53. theorem OAI.LaughlinFock.fourYNumber_20_19_5 line 250
  54. theorem OAI.LaughlinFock.fourYNumber_20_19_7 line 254
  55. theorem OAI.LaughlinFock.fourYNumber_20_19_9 line 258
  56. theorem OAI.LaughlinFock.fourYNumber_20_19_11 line 262
  57. theorem OAI.LaughlinFock.fourYNumber_20_19_13 line 266
  58. theorem OAI.LaughlinFock.fourYNumber_20_19_15 line 270
  59. theorem OAI.LaughlinFock.fourYNumber_20_19_17 line 274
  60. theorem OAI.LaughlinFock.fourYNumber_20_19_19 line 278