OAI/Analysis/LaughlinFock/Sparse1122.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Sparse1122.

  1. def OAI.LaughlinFock.collectedFourData_11_6 line 11
  2. theorem OAI.LaughlinFock.collectedFourChecked_11_6 line 64
  3. def OAI.LaughlinFock.collectedFourData_11_7_0 line 67
  4. def OAI.LaughlinFock.collectedFourData_11_7_1 line 85
  5. def OAI.LaughlinFock.collectedFourData_11_7_2 line 109
  6. def OAI.LaughlinFock.collectedFourData_11_7_3 line 127
  7. def OAI.LaughlinFock.collectedFourData_11_7_4 line 151
  8. def OAI.LaughlinFock.collectedFourData_11_7_5 line 182
  9. def OAI.LaughlinFock.collectedFourData_11_7_6 line 200
  10. def OAI.LaughlinFock.collectedFourData_11_7_7 line 224
  11. def OAI.LaughlinFock.collectedFourData_11_7_8 line 255
  12. def OAI.LaughlinFock.collectedFourData_11_7_9 line 294
  13. def OAI.LaughlinFock.collectedFourData_11_7_10 line 312
  14. def OAI.LaughlinFock.collectedFourData_11_7_11 line 336
  15. def OAI.LaughlinFock.collectedFourData_11_7_12 line 367
  16. def OAI.LaughlinFock.collectedFourData_11_7_13 line 406
  17. def OAI.LaughlinFock.collectedFourData_11_7_14 line 453
  18. def OAI.LaughlinFock.collectedFourData_11_7_15 line 471
  19. def OAI.LaughlinFock.collectedFourData_11_7_16 line 495
  20. def OAI.LaughlinFock.collectedFourData_11_7_17 line 526
  21. def OAI.LaughlinFock.collectedFourData_11_7_18 line 565