OAI/Analysis/LaughlinFock/Sparse0927.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Sparse0927.

  1. def OAI.LaughlinFock.collectedFourData_9_6_42 line 11
  2. def OAI.LaughlinFock.collectedFourData_9_6_43 line 49
  3. def OAI.LaughlinFock.collectedFourData_9_6_44 line 95
  4. def OAI.LaughlinFock.collectedFourData_9_6_45 line 148
  5. def OAI.LaughlinFock.collectedFourData_9_6_46 line 201
  6. def OAI.LaughlinFock.collectedFourData_9_6_47 line 254
  7. def OAI.LaughlinFock.collectedFourData_9_6_48 line 307
  8. def OAI.LaughlinFock.collectedFourData_9_6_49 line 360
  9. def OAI.LaughlinFock.collectedFourData_9_6 line 413
  10. theorem OAI.LaughlinFock.collectedFourChecked_9_6 line 466
  11. def OAI.LaughlinFock.collectedFourData_9_7_0 line 469
  12. def OAI.LaughlinFock.collectedFourData_9_7_1 line 500
  13. def OAI.LaughlinFock.collectedFourData_9_7_2 line 539
  14. def OAI.LaughlinFock.collectedFourData_9_7_3 line 570
  15. def OAI.LaughlinFock.collectedFourData_9_7_4 line 609