OAI/Analysis/LaughlinFock/Sparse0903.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Sparse0903.

  1. def OAI.LaughlinFock.collectedFourData_9_0_37 line 10
  2. def OAI.LaughlinFock.collectedFourData_9_0_38 line 54
  3. def OAI.LaughlinFock.collectedFourData_9_0_39 line 100
  4. def OAI.LaughlinFock.collectedFourData_9_0_40 line 141
  5. def OAI.LaughlinFock.collectedFourData_9_0_41 line 185
  6. def OAI.LaughlinFock.collectedFourData_9_0_42 line 231
  7. def OAI.LaughlinFock.collectedFourData_9_0_43 line 275
  8. def OAI.LaughlinFock.collectedFourData_9_0 line 321
  9. theorem OAI.LaughlinFock.collectedFourChecked_9_0 line 368
  10. def OAI.LaughlinFock.collectedFourData_9_1_0 line 371
  11. def OAI.LaughlinFock.collectedFourData_9_1_1 line 381
  12. def OAI.LaughlinFock.collectedFourData_9_1_2 line 399
  13. def OAI.LaughlinFock.collectedFourData_9_1_3 line 425
  14. def OAI.LaughlinFock.collectedFourData_9_1_4 line 458
  15. def OAI.LaughlinFock.collectedFourData_9_1_5 line 497
  16. def OAI.LaughlinFock.collectedFourData_9_1_6 line 541
  17. def OAI.LaughlinFock.collectedFourData_9_1_7 line 589