OAI/Analysis/LaughlinFock/Certificate13Data.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Certificate13 Data.

  1. def OAI.LaughlinFock.fourYData_13 line 14
  2. def OAI.LaughlinFock.fourZData_13 line 25
  3. def OAI.LaughlinFock.fourLData_13 line 36
  4. def OAI.LaughlinFock.fourPivotData_13 line 47
  5. theorem OAI.LaughlinFock.fourOccupations_13 line 50
  6. theorem OAI.LaughlinFock.fourYNumber_13_1_1 line 53
  7. theorem OAI.LaughlinFock.fourYNumber_13_3_1 line 57
  8. theorem OAI.LaughlinFock.fourYNumber_13_3_3 line 61
  9. theorem OAI.LaughlinFock.fourYNumber_13_5_1 line 65
  10. theorem OAI.LaughlinFock.fourYNumber_13_5_3 line 69
  11. theorem OAI.LaughlinFock.fourYNumber_13_5_5 line 73
  12. theorem OAI.LaughlinFock.fourYNumber_13_7_1 line 77
  13. theorem OAI.LaughlinFock.fourYNumber_13_7_3 line 81
  14. theorem OAI.LaughlinFock.fourYNumber_13_7_5 line 85
  15. theorem OAI.LaughlinFock.fourYNumber_13_7_7 line 89
  16. theorem OAI.LaughlinFock.fourYNumber_13_9_1 line 93
  17. theorem OAI.LaughlinFock.fourYNumber_13_9_3 line 97
  18. theorem OAI.LaughlinFock.fourYNumber_13_9_5 line 101
  19. theorem OAI.LaughlinFock.fourYNumber_13_9_7 line 105
  20. theorem OAI.LaughlinFock.fourYNumber_13_9_9 line 109
  21. theorem OAI.LaughlinFock.fourYNumber_13_11_1 line 113
  22. theorem OAI.LaughlinFock.fourYNumber_13_11_3 line 117
  23. theorem OAI.LaughlinFock.fourYNumber_13_11_5 line 121
  24. theorem OAI.LaughlinFock.fourYNumber_13_11_7 line 125
  25. theorem OAI.LaughlinFock.fourYNumber_13_11_9 line 129
  26. theorem OAI.LaughlinFock.fourYNumber_13_11_11 line 133
  27. theorem OAI.LaughlinFock.fourYNumber_13_13_1 line 137
  28. theorem OAI.LaughlinFock.fourYNumber_13_13_3 line 141
  29. theorem OAI.LaughlinFock.fourYNumber_13_13_5 line 145
  30. theorem OAI.LaughlinFock.fourYNumber_13_13_7 line 149
  31. theorem OAI.LaughlinFock.fourYNumber_13_13_9 line 153
  32. theorem OAI.LaughlinFock.fourYNumber_13_13_11 line 157
  33. theorem OAI.LaughlinFock.fourYNumber_13_13_13 line 161