OAI/Analysis/LaughlinFock/Sparse1310.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Sparse1310.

  1. def OAI.LaughlinFock.collectedFourData_13_4_43 line 9
  2. def OAI.LaughlinFock.collectedFourData_13_4_44 line 21
  3. def OAI.LaughlinFock.collectedFourData_13_4_45 line 39
  4. def OAI.LaughlinFock.collectedFourData_13_4_46 line 64
  5. def OAI.LaughlinFock.collectedFourData_13_4_47 line 97
  6. def OAI.LaughlinFock.collectedFourData_13_4_48 line 138
  7. def OAI.LaughlinFock.collectedFourData_13_4_49 line 186
  8. def OAI.LaughlinFock.collectedFourData_13_4_50 line 240
  9. def OAI.LaughlinFock.collectedFourData_13_4_51 line 258
  10. def OAI.LaughlinFock.collectedFourData_13_4_52 line 283
  11. def OAI.LaughlinFock.collectedFourData_13_4_53 line 316
  12. def OAI.LaughlinFock.collectedFourData_13_4_54 line 357
  13. def OAI.LaughlinFock.collectedFourData_13_4_55 line 405
  14. def OAI.LaughlinFock.collectedFourData_13_4 line 459
  15. theorem OAI.LaughlinFock.collectedFourChecked_13_4 line 518
  16. def OAI.LaughlinFock.collectedFourData_13_5_0 line 521
  17. def OAI.LaughlinFock.collectedFourData_13_5_1 line 527
  18. def OAI.LaughlinFock.collectedFourData_13_5_2 line 537
  19. def OAI.LaughlinFock.collectedFourData_13_5_3 line 552
  20. def OAI.LaughlinFock.collectedFourData_13_5_4 line 573
  21. def OAI.LaughlinFock.collectedFourData_13_5_5 line 579
  22. def OAI.LaughlinFock.collectedFourData_13_5_6 line 589
  23. def OAI.LaughlinFock.collectedFourData_13_5_7 line 604