OAI/Analysis/LaughlinFock/Sparse1306.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Sparse1306.

  1. def OAI.LaughlinFock.collectedFourData_13_2 line 10
  2. theorem OAI.LaughlinFock.collectedFourChecked_13_2 line 67
  3. def OAI.LaughlinFock.collectedFourData_13_3_0 line 70
  4. def OAI.LaughlinFock.collectedFourData_13_3_1 line 74
  5. def OAI.LaughlinFock.collectedFourData_13_3_2 line 78
  6. def OAI.LaughlinFock.collectedFourData_13_3_3 line 86
  7. def OAI.LaughlinFock.collectedFourData_13_3_4 line 100
  8. def OAI.LaughlinFock.collectedFourData_13_3_5 line 121
  9. def OAI.LaughlinFock.collectedFourData_13_3_6 line 150
  10. def OAI.LaughlinFock.collectedFourData_13_3_7 line 154
  11. def OAI.LaughlinFock.collectedFourData_13_3_8 line 158
  12. def OAI.LaughlinFock.collectedFourData_13_3_9 line 166
  13. def OAI.LaughlinFock.collectedFourData_13_3_10 line 180
  14. def OAI.LaughlinFock.collectedFourData_13_3_11 line 201
  15. def OAI.LaughlinFock.collectedFourData_13_3_12 line 230
  16. def OAI.LaughlinFock.collectedFourData_13_3_13 line 267
  17. def OAI.LaughlinFock.collectedFourData_13_3_14 line 271
  18. def OAI.LaughlinFock.collectedFourData_13_3_15 line 275
  19. def OAI.LaughlinFock.collectedFourData_13_3_16 line 283
  20. def OAI.LaughlinFock.collectedFourData_13_3_17 line 297
  21. def OAI.LaughlinFock.collectedFourData_13_3_18 line 318
  22. def OAI.LaughlinFock.collectedFourData_13_3_19 line 347
  23. def OAI.LaughlinFock.collectedFourData_13_3_20 line 384
  24. def OAI.LaughlinFock.collectedFourData_13_3_21 line 428
  25. def OAI.LaughlinFock.collectedFourData_13_3_22 line 432
  26. def OAI.LaughlinFock.collectedFourData_13_3_23 line 436
  27. def OAI.LaughlinFock.collectedFourData_13_3_24 line 444
  28. def OAI.LaughlinFock.collectedFourData_13_3_25 line 458
  29. def OAI.LaughlinFock.collectedFourData_13_3_26 line 479
  30. def OAI.LaughlinFock.collectedFourData_13_3_27 line 508
  31. def OAI.LaughlinFock.collectedFourData_13_3_28 line 545
  32. def OAI.LaughlinFock.collectedFourData_13_3_29 line 589