OAI/Analysis/LaughlinFock/Sparse1403.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Sparse1403.

  1. def OAI.LaughlinFock.collectedFourData_14_1_47 line 9
  2. def OAI.LaughlinFock.collectedFourData_14_1_48 line 27
  3. def OAI.LaughlinFock.collectedFourData_14_1_49 line 53
  4. def OAI.LaughlinFock.collectedFourData_14_1 line 86
  5. theorem OAI.LaughlinFock.collectedFourChecked_14_1 line 139
  6. def OAI.LaughlinFock.collectedFourData_14_2_0 line 142
  7. def OAI.LaughlinFock.collectedFourData_14_2_1 line 146
  8. def OAI.LaughlinFock.collectedFourData_14_2_2 line 150
  9. def OAI.LaughlinFock.collectedFourData_14_2_3 line 154
  10. def OAI.LaughlinFock.collectedFourData_14_2_4 line 158
  11. def OAI.LaughlinFock.collectedFourData_14_2_5 line 167
  12. def OAI.LaughlinFock.collectedFourData_14_2_6 line 183
  13. def OAI.LaughlinFock.collectedFourData_14_2_7 line 207
  14. def OAI.LaughlinFock.collectedFourData_14_2_8 line 211
  15. def OAI.LaughlinFock.collectedFourData_14_2_9 line 215
  16. def OAI.LaughlinFock.collectedFourData_14_2_10 line 219
  17. def OAI.LaughlinFock.collectedFourData_14_2_11 line 223
  18. def OAI.LaughlinFock.collectedFourData_14_2_12 line 232
  19. def OAI.LaughlinFock.collectedFourData_14_2_13 line 248
  20. def OAI.LaughlinFock.collectedFourData_14_2_14 line 272
  21. def OAI.LaughlinFock.collectedFourData_14_2_15 line 304
  22. def OAI.LaughlinFock.collectedFourData_14_2_16 line 308
  23. def OAI.LaughlinFock.collectedFourData_14_2_17 line 312
  24. def OAI.LaughlinFock.collectedFourData_14_2_18 line 316
  25. def OAI.LaughlinFock.collectedFourData_14_2_19 line 320
  26. def OAI.LaughlinFock.collectedFourData_14_2_20 line 329
  27. def OAI.LaughlinFock.collectedFourData_14_2_21 line 345
  28. def OAI.LaughlinFock.collectedFourData_14_2_22 line 369
  29. def OAI.LaughlinFock.collectedFourData_14_2_23 line 401
  30. def OAI.LaughlinFock.collectedFourData_14_2_24 line 440
  31. def OAI.LaughlinFock.collectedFourData_14_2_25 line 444
  32. def OAI.LaughlinFock.collectedFourData_14_2_26 line 448
  33. def OAI.LaughlinFock.collectedFourData_14_2_27 line 452
  34. def OAI.LaughlinFock.collectedFourData_14_2_28 line 461
  35. def OAI.LaughlinFock.collectedFourData_14_2_29 line 477
  36. def OAI.LaughlinFock.collectedFourData_14_2_30 line 501
  37. def OAI.LaughlinFock.collectedFourData_14_2_31 line 533
  38. def OAI.LaughlinFock.collectedFourData_14_2_32 line 572
  39. def OAI.LaughlinFock.collectedFourData_14_2_33 line 576
  40. def OAI.LaughlinFock.collectedFourData_14_2_34 line 580
  41. def OAI.LaughlinFock.collectedFourData_14_2_35 line 589
  42. def OAI.LaughlinFock.collectedFourData_14_2_36 line 605