OAI/Analysis/LaughlinFock/Sparse1108.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Sparse1108.

  1. def OAI.LaughlinFock.collectedFourData_11_2_47 line 10
  2. def OAI.LaughlinFock.collectedFourData_11_2_48 line 55
  3. def OAI.LaughlinFock.collectedFourData_11_2_49 line 105
  4. def OAI.LaughlinFock.collectedFourData_11_2_50 line 159
  5. def OAI.LaughlinFock.collectedFourData_11_2_51 line 198
  6. def OAI.LaughlinFock.collectedFourData_11_2_52 line 243
  7. def OAI.LaughlinFock.collectedFourData_11_2_53 line 293
  8. def OAI.LaughlinFock.collectedFourData_11_2 line 347
  9. theorem OAI.LaughlinFock.collectedFourChecked_11_2 line 404
  10. def OAI.LaughlinFock.collectedFourData_11_3_0 line 407
  11. def OAI.LaughlinFock.collectedFourData_11_3_1 line 415
  12. def OAI.LaughlinFock.collectedFourData_11_3_2 line 429
  13. def OAI.LaughlinFock.collectedFourData_11_3_3 line 450
  14. def OAI.LaughlinFock.collectedFourData_11_3_4 line 479
  15. def OAI.LaughlinFock.collectedFourData_11_3_5 line 516
  16. def OAI.LaughlinFock.collectedFourData_11_3_6 line 560
  17. def OAI.LaughlinFock.collectedFourData_11_3_7 line 568
  18. def OAI.LaughlinFock.collectedFourData_11_3_8 line 582
  19. def OAI.LaughlinFock.collectedFourData_11_3_9 line 603