OAI/Analysis/LaughlinFock/Certificate18Data.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Certificate18 Data.

  1. def OAI.LaughlinFock.fourYData_18 line 14
  2. def OAI.LaughlinFock.fourZData_18 line 27
  3. def OAI.LaughlinFock.fourLData_18 line 40
  4. def OAI.LaughlinFock.fourPivotData_18 line 53
  5. theorem OAI.LaughlinFock.fourOccupations_18 line 56
  6. theorem OAI.LaughlinFock.fourYNumber_18_1_1 line 59
  7. theorem OAI.LaughlinFock.fourYNumber_18_3_1 line 63
  8. theorem OAI.LaughlinFock.fourYNumber_18_3_3 line 67
  9. theorem OAI.LaughlinFock.fourYNumber_18_5_1 line 71
  10. theorem OAI.LaughlinFock.fourYNumber_18_5_3 line 75
  11. theorem OAI.LaughlinFock.fourYNumber_18_5_5 line 79
  12. theorem OAI.LaughlinFock.fourYNumber_18_7_1 line 83
  13. theorem OAI.LaughlinFock.fourYNumber_18_7_3 line 87
  14. theorem OAI.LaughlinFock.fourYNumber_18_7_5 line 91
  15. theorem OAI.LaughlinFock.fourYNumber_18_7_7 line 95
  16. theorem OAI.LaughlinFock.fourYNumber_18_9_1 line 99
  17. theorem OAI.LaughlinFock.fourYNumber_18_9_3 line 103
  18. theorem OAI.LaughlinFock.fourYNumber_18_9_5 line 107
  19. theorem OAI.LaughlinFock.fourYNumber_18_9_7 line 111
  20. theorem OAI.LaughlinFock.fourYNumber_18_9_9 line 115
  21. theorem OAI.LaughlinFock.fourYNumber_18_11_1 line 119
  22. theorem OAI.LaughlinFock.fourYNumber_18_11_3 line 123
  23. theorem OAI.LaughlinFock.fourYNumber_18_11_5 line 127
  24. theorem OAI.LaughlinFock.fourYNumber_18_11_7 line 131
  25. theorem OAI.LaughlinFock.fourYNumber_18_11_9 line 135
  26. theorem OAI.LaughlinFock.fourYNumber_18_11_11 line 139
  27. theorem OAI.LaughlinFock.fourYNumber_18_13_1 line 143
  28. theorem OAI.LaughlinFock.fourYNumber_18_13_3 line 147
  29. theorem OAI.LaughlinFock.fourYNumber_18_13_5 line 151
  30. theorem OAI.LaughlinFock.fourYNumber_18_13_7 line 155
  31. theorem OAI.LaughlinFock.fourYNumber_18_13_9 line 159
  32. theorem OAI.LaughlinFock.fourYNumber_18_13_11 line 163
  33. theorem OAI.LaughlinFock.fourYNumber_18_13_13 line 167
  34. theorem OAI.LaughlinFock.fourYNumber_18_15_1 line 171
  35. theorem OAI.LaughlinFock.fourYNumber_18_15_3 line 175
  36. theorem OAI.LaughlinFock.fourYNumber_18_15_5 line 179
  37. theorem OAI.LaughlinFock.fourYNumber_18_15_7 line 183
  38. theorem OAI.LaughlinFock.fourYNumber_18_15_9 line 187
  39. theorem OAI.LaughlinFock.fourYNumber_18_15_11 line 191
  40. theorem OAI.LaughlinFock.fourYNumber_18_15_13 line 195
  41. theorem OAI.LaughlinFock.fourYNumber_18_15_15 line 199
  42. theorem OAI.LaughlinFock.fourYNumber_18_17_1 line 203
  43. theorem OAI.LaughlinFock.fourYNumber_18_17_3 line 207
  44. theorem OAI.LaughlinFock.fourYNumber_18_17_5 line 211
  45. theorem OAI.LaughlinFock.fourYNumber_18_17_7 line 215
  46. theorem OAI.LaughlinFock.fourYNumber_18_17_9 line 219
  47. theorem OAI.LaughlinFock.fourYNumber_18_17_11 line 223
  48. theorem OAI.LaughlinFock.fourYNumber_18_17_13 line 227
  49. theorem OAI.LaughlinFock.fourYNumber_18_17_15 line 231
  50. theorem OAI.LaughlinFock.fourYNumber_18_17_17 line 235