OAI/Analysis/LaughlinFock/Certificate16Data.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Certificate16 Data.

  1. def OAI.LaughlinFock.fourYData_16 line 14
  2. def OAI.LaughlinFock.fourZData_16 line 26
  3. def OAI.LaughlinFock.fourLData_16 line 38
  4. def OAI.LaughlinFock.fourPivotData_16 line 50
  5. theorem OAI.LaughlinFock.fourOccupations_16 line 53
  6. theorem OAI.LaughlinFock.fourYNumber_16_1_1 line 56
  7. theorem OAI.LaughlinFock.fourYNumber_16_3_1 line 60
  8. theorem OAI.LaughlinFock.fourYNumber_16_3_3 line 64
  9. theorem OAI.LaughlinFock.fourYNumber_16_5_1 line 68
  10. theorem OAI.LaughlinFock.fourYNumber_16_5_3 line 72
  11. theorem OAI.LaughlinFock.fourYNumber_16_5_5 line 76
  12. theorem OAI.LaughlinFock.fourYNumber_16_7_1 line 80
  13. theorem OAI.LaughlinFock.fourYNumber_16_7_3 line 84
  14. theorem OAI.LaughlinFock.fourYNumber_16_7_5 line 88
  15. theorem OAI.LaughlinFock.fourYNumber_16_7_7 line 92
  16. theorem OAI.LaughlinFock.fourYNumber_16_9_1 line 96
  17. theorem OAI.LaughlinFock.fourYNumber_16_9_3 line 100
  18. theorem OAI.LaughlinFock.fourYNumber_16_9_5 line 104
  19. theorem OAI.LaughlinFock.fourYNumber_16_9_7 line 108
  20. theorem OAI.LaughlinFock.fourYNumber_16_9_9 line 112
  21. theorem OAI.LaughlinFock.fourYNumber_16_11_1 line 116
  22. theorem OAI.LaughlinFock.fourYNumber_16_11_3 line 120
  23. theorem OAI.LaughlinFock.fourYNumber_16_11_5 line 124
  24. theorem OAI.LaughlinFock.fourYNumber_16_11_7 line 128
  25. theorem OAI.LaughlinFock.fourYNumber_16_11_9 line 132
  26. theorem OAI.LaughlinFock.fourYNumber_16_11_11 line 136
  27. theorem OAI.LaughlinFock.fourYNumber_16_13_1 line 140
  28. theorem OAI.LaughlinFock.fourYNumber_16_13_3 line 144
  29. theorem OAI.LaughlinFock.fourYNumber_16_13_5 line 148
  30. theorem OAI.LaughlinFock.fourYNumber_16_13_7 line 152
  31. theorem OAI.LaughlinFock.fourYNumber_16_13_9 line 156
  32. theorem OAI.LaughlinFock.fourYNumber_16_13_11 line 160
  33. theorem OAI.LaughlinFock.fourYNumber_16_13_13 line 164
  34. theorem OAI.LaughlinFock.fourYNumber_16_15_1 line 168
  35. theorem OAI.LaughlinFock.fourYNumber_16_15_3 line 172
  36. theorem OAI.LaughlinFock.fourYNumber_16_15_5 line 176
  37. theorem OAI.LaughlinFock.fourYNumber_16_15_7 line 180
  38. theorem OAI.LaughlinFock.fourYNumber_16_15_9 line 184
  39. theorem OAI.LaughlinFock.fourYNumber_16_15_11 line 188
  40. theorem OAI.LaughlinFock.fourYNumber_16_15_13 line 192
  41. theorem OAI.LaughlinFock.fourYNumber_16_15_15 line 196