OAI/Analysis/LaughlinFock/Sparse1401.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Sparse1401.

  1. def OAI.LaughlinFock.collectedFourData_14_0_0 line 9
  2. def OAI.LaughlinFock.collectedFourData_14_0_1 line 13
  3. def OAI.LaughlinFock.collectedFourData_14_0_2 line 17
  4. def OAI.LaughlinFock.collectedFourData_14_0_3 line 21
  5. def OAI.LaughlinFock.collectedFourData_14_0_4 line 25
  6. def OAI.LaughlinFock.collectedFourData_14_0_5 line 29
  7. def OAI.LaughlinFock.collectedFourData_14_0_6 line 33
  8. def OAI.LaughlinFock.collectedFourData_14_0_7 line 44
  9. def OAI.LaughlinFock.collectedFourData_14_0_8 line 63
  10. def OAI.LaughlinFock.collectedFourData_14_0_9 line 89
  11. def OAI.LaughlinFock.collectedFourData_14_0_10 line 93
  12. def OAI.LaughlinFock.collectedFourData_14_0_11 line 97
  13. def OAI.LaughlinFock.collectedFourData_14_0_12 line 101
  14. def OAI.LaughlinFock.collectedFourData_14_0_13 line 105
  15. def OAI.LaughlinFock.collectedFourData_14_0_14 line 109
  16. def OAI.LaughlinFock.collectedFourData_14_0_15 line 120
  17. def OAI.LaughlinFock.collectedFourData_14_0_16 line 139
  18. def OAI.LaughlinFock.collectedFourData_14_0_17 line 165
  19. def OAI.LaughlinFock.collectedFourData_14_0_18 line 169
  20. def OAI.LaughlinFock.collectedFourData_14_0_19 line 173
  21. def OAI.LaughlinFock.collectedFourData_14_0_20 line 177
  22. def OAI.LaughlinFock.collectedFourData_14_0_21 line 181
  23. def OAI.LaughlinFock.collectedFourData_14_0_22 line 192
  24. def OAI.LaughlinFock.collectedFourData_14_0_23 line 211
  25. def OAI.LaughlinFock.collectedFourData_14_0_24 line 237
  26. def OAI.LaughlinFock.collectedFourData_14_0_25 line 241
  27. def OAI.LaughlinFock.collectedFourData_14_0_26 line 245
  28. def OAI.LaughlinFock.collectedFourData_14_0_27 line 249
  29. def OAI.LaughlinFock.collectedFourData_14_0_28 line 260
  30. def OAI.LaughlinFock.collectedFourData_14_0_29 line 279
  31. def OAI.LaughlinFock.collectedFourData_14_0_30 line 305
  32. def OAI.LaughlinFock.collectedFourData_14_0_31 line 309
  33. def OAI.LaughlinFock.collectedFourData_14_0_32 line 313
  34. def OAI.LaughlinFock.collectedFourData_14_0_33 line 324
  35. def OAI.LaughlinFock.collectedFourData_14_0_34 line 343
  36. def OAI.LaughlinFock.collectedFourData_14_0_35 line 369
  37. def OAI.LaughlinFock.collectedFourData_14_0_36 line 373
  38. def OAI.LaughlinFock.collectedFourData_14_0_37 line 384
  39. def OAI.LaughlinFock.collectedFourData_14_0_38 line 403
  40. def OAI.LaughlinFock.collectedFourData_14_0_39 line 429
  41. def OAI.LaughlinFock.collectedFourData_14_0_40 line 440
  42. def OAI.LaughlinFock.collectedFourData_14_0_41 line 459
  43. def OAI.LaughlinFock.collectedFourData_14_0_42 line 485
  44. def OAI.LaughlinFock.collectedFourData_14_0_43 line 504
  45. def OAI.LaughlinFock.collectedFourData_14_0 line 530
  46. theorem OAI.LaughlinFock.collectedFourChecked_14_0 line 577
  47. def OAI.LaughlinFock.collectedFourData_14_1_0 line 580
  48. def OAI.LaughlinFock.collectedFourData_14_1_1 line 584
  49. def OAI.LaughlinFock.collectedFourData_14_1_2 line 588
  50. def OAI.LaughlinFock.collectedFourData_14_1_3 line 592
  51. def OAI.LaughlinFock.collectedFourData_14_1_4 line 596
  52. def OAI.LaughlinFock.collectedFourData_14_1_5 line 600