OAI/Analysis/LaughlinFock/Sparse1303.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Sparse1303.

  1. def OAI.LaughlinFock.collectedFourData_13_1_30 line 8
  2. def OAI.LaughlinFock.collectedFourData_13_1_31 line 41
  3. def OAI.LaughlinFock.collectedFourData_13_1_32 line 80
  4. def OAI.LaughlinFock.collectedFourData_13_1_33 line 84
  5. def OAI.LaughlinFock.collectedFourData_13_1_34 line 94
  6. def OAI.LaughlinFock.collectedFourData_13_1_35 line 112
  7. def OAI.LaughlinFock.collectedFourData_13_1_36 line 138
  8. def OAI.LaughlinFock.collectedFourData_13_1_37 line 171
  9. def OAI.LaughlinFock.collectedFourData_13_1_38 line 210
  10. def OAI.LaughlinFock.collectedFourData_13_1_39 line 220
  11. def OAI.LaughlinFock.collectedFourData_13_1_40 line 238
  12. def OAI.LaughlinFock.collectedFourData_13_1_41 line 264
  13. def OAI.LaughlinFock.collectedFourData_13_1_42 line 297
  14. def OAI.LaughlinFock.collectedFourData_13_1_43 line 336
  15. def OAI.LaughlinFock.collectedFourData_13_1_44 line 354
  16. def OAI.LaughlinFock.collectedFourData_13_1_45 line 380
  17. def OAI.LaughlinFock.collectedFourData_13_1_46 line 413
  18. def OAI.LaughlinFock.collectedFourData_13_1_47 line 452
  19. def OAI.LaughlinFock.collectedFourData_13_1_48 line 478
  20. def OAI.LaughlinFock.collectedFourData_13_1_49 line 511
  21. def OAI.LaughlinFock.collectedFourData_13_1 line 550
  22. theorem OAI.LaughlinFock.collectedFourChecked_13_1 line 603
  23. def OAI.LaughlinFock.collectedFourData_13_2_0 line 606