OAI/Analysis/LaughlinFock/Sparse1105.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Sparse1105.

  1. def OAI.LaughlinFock.collectedFourData_11_1_43 line 10
  2. def OAI.LaughlinFock.collectedFourData_11_1_44 line 43
  3. def OAI.LaughlinFock.collectedFourData_11_1_45 line 82
  4. def OAI.LaughlinFock.collectedFourData_11_1_46 line 126
  5. def OAI.LaughlinFock.collectedFourData_11_1_47 line 174
  6. def OAI.LaughlinFock.collectedFourData_11_1_48 line 213
  7. def OAI.LaughlinFock.collectedFourData_11_1_49 line 257
  8. def OAI.LaughlinFock.collectedFourData_11_1 line 305
  9. theorem OAI.LaughlinFock.collectedFourChecked_11_1 line 358
  10. def OAI.LaughlinFock.collectedFourData_11_2_0 line 361
  11. def OAI.LaughlinFock.collectedFourData_11_2_1 line 365
  12. def OAI.LaughlinFock.collectedFourData_11_2_2 line 374
  13. def OAI.LaughlinFock.collectedFourData_11_2_3 line 390
  14. def OAI.LaughlinFock.collectedFourData_11_2_4 line 414
  15. def OAI.LaughlinFock.collectedFourData_11_2_5 line 446
  16. def OAI.LaughlinFock.collectedFourData_11_2_6 line 485
  17. def OAI.LaughlinFock.collectedFourData_11_2_7 line 530
  18. def OAI.LaughlinFock.collectedFourData_11_2_8 line 534
  19. def OAI.LaughlinFock.collectedFourData_11_2_9 line 543
  20. def OAI.LaughlinFock.collectedFourData_11_2_10 line 559
  21. def OAI.LaughlinFock.collectedFourData_11_2_11 line 583