OAI/Analysis/LaughlinFock/Sparse0830.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Sparse0830.

  1. def OAI.LaughlinFock.collectedFourData_8_6 line 11
  2. theorem OAI.LaughlinFock.collectedFourChecked_8_6 line 64
  3. def OAI.LaughlinFock.collectedFourData_8_7_0 line 67
  4. def OAI.LaughlinFock.collectedFourData_8_7_1 line 106
  5. def OAI.LaughlinFock.collectedFourData_8_7_2 line 153
  6. def OAI.LaughlinFock.collectedFourData_8_7_3 line 192
  7. def OAI.LaughlinFock.collectedFourData_8_7_4 line 239
  8. def OAI.LaughlinFock.collectedFourData_8_7_5 line 286
  9. def OAI.LaughlinFock.collectedFourData_8_7_6 line 325
  10. def OAI.LaughlinFock.collectedFourData_8_7_7 line 372
  11. def OAI.LaughlinFock.collectedFourData_8_7_8 line 419
  12. def OAI.LaughlinFock.collectedFourData_8_7_9 line 466
  13. def OAI.LaughlinFock.collectedFourData_8_7_10 line 505
  14. def OAI.LaughlinFock.collectedFourData_8_7_11 line 552
  15. def OAI.LaughlinFock.collectedFourData_8_7_12 line 599