OAI/Analysis/LaughlinFock/Sparse1315.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Sparse1315.

  1. def OAI.LaughlinFock.collectedFourData_13_6_47 line 9
  2. def OAI.LaughlinFock.collectedFourData_13_6_48 line 55
  3. def OAI.LaughlinFock.collectedFourData_13_6_49 line 108
  4. def OAI.LaughlinFock.collectedFourData_13_6 line 161
  5. theorem OAI.LaughlinFock.collectedFourChecked_13_6 line 214
  6. def OAI.LaughlinFock.collectedFourData_13_7_0 line 217
  7. def OAI.LaughlinFock.collectedFourData_13_7_1 line 226
  8. def OAI.LaughlinFock.collectedFourData_13_7_2 line 239
  9. def OAI.LaughlinFock.collectedFourData_13_7_3 line 248
  10. def OAI.LaughlinFock.collectedFourData_13_7_4 line 261
  11. def OAI.LaughlinFock.collectedFourData_13_7_5 line 279
  12. def OAI.LaughlinFock.collectedFourData_13_7_6 line 288
  13. def OAI.LaughlinFock.collectedFourData_13_7_7 line 301
  14. def OAI.LaughlinFock.collectedFourData_13_7_8 line 319
  15. def OAI.LaughlinFock.collectedFourData_13_7_9 line 343
  16. def OAI.LaughlinFock.collectedFourData_13_7_10 line 352
  17. def OAI.LaughlinFock.collectedFourData_13_7_11 line 365
  18. def OAI.LaughlinFock.collectedFourData_13_7_12 line 383
  19. def OAI.LaughlinFock.collectedFourData_13_7_13 line 407
  20. def OAI.LaughlinFock.collectedFourData_13_7_14 line 438
  21. def OAI.LaughlinFock.collectedFourData_13_7_15 line 447
  22. def OAI.LaughlinFock.collectedFourData_13_7_16 line 460
  23. def OAI.LaughlinFock.collectedFourData_13_7_17 line 478
  24. def OAI.LaughlinFock.collectedFourData_13_7_18 line 502
  25. def OAI.LaughlinFock.collectedFourData_13_7_19 line 533
  26. def OAI.LaughlinFock.collectedFourData_13_7_20 line 572
  27. def OAI.LaughlinFock.collectedFourData_13_7_21 line 581
  28. def OAI.LaughlinFock.collectedFourData_13_7_22 line 594