OAI/Analysis/LaughlinFock/Sparse0919.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Sparse0919.

  1. def OAI.LaughlinFock.collectedFourData_9_4_49 line 11
  2. def OAI.LaughlinFock.collectedFourData_9_4_50 line 70
  3. def OAI.LaughlinFock.collectedFourData_9_4_51 line 118
  4. def OAI.LaughlinFock.collectedFourData_9_4_52 line 172
  5. def OAI.LaughlinFock.collectedFourData_9_4_53 line 231
  6. def OAI.LaughlinFock.collectedFourData_9_4_54 line 290
  7. def OAI.LaughlinFock.collectedFourData_9_4_55 line 349
  8. def OAI.LaughlinFock.collectedFourData_9_4 line 408
  9. theorem OAI.LaughlinFock.collectedFourChecked_9_4 line 467
  10. def OAI.LaughlinFock.collectedFourData_9_5_0 line 470
  11. def OAI.LaughlinFock.collectedFourData_9_5_1 line 498
  12. def OAI.LaughlinFock.collectedFourData_9_5_2 line 534
  13. def OAI.LaughlinFock.collectedFourData_9_5_3 line 578