OAI/Analysis/LaughlinFock/Sparse1313.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Sparse1313.

  1. def OAI.LaughlinFock.collectedFourData_13_5_53 line 10
  2. def OAI.LaughlinFock.collectedFourData_13_5 line 67
  3. theorem OAI.LaughlinFock.collectedFourChecked_13_5 line 124
  4. def OAI.LaughlinFock.collectedFourData_13_6_0 line 127
  5. def OAI.LaughlinFock.collectedFourData_13_6_1 line 135
  6. def OAI.LaughlinFock.collectedFourData_13_6_2 line 147
  7. def OAI.LaughlinFock.collectedFourData_13_6_3 line 164
  8. def OAI.LaughlinFock.collectedFourData_13_6_4 line 172
  9. def OAI.LaughlinFock.collectedFourData_13_6_5 line 184
  10. def OAI.LaughlinFock.collectedFourData_13_6_6 line 201
  11. def OAI.LaughlinFock.collectedFourData_13_6_7 line 224
  12. def OAI.LaughlinFock.collectedFourData_13_6_8 line 232
  13. def OAI.LaughlinFock.collectedFourData_13_6_9 line 244
  14. def OAI.LaughlinFock.collectedFourData_13_6_10 line 261
  15. def OAI.LaughlinFock.collectedFourData_13_6_11 line 284
  16. def OAI.LaughlinFock.collectedFourData_13_6_12 line 314
  17. def OAI.LaughlinFock.collectedFourData_13_6_13 line 322
  18. def OAI.LaughlinFock.collectedFourData_13_6_14 line 334
  19. def OAI.LaughlinFock.collectedFourData_13_6_15 line 351
  20. def OAI.LaughlinFock.collectedFourData_13_6_16 line 374
  21. def OAI.LaughlinFock.collectedFourData_13_6_17 line 404
  22. def OAI.LaughlinFock.collectedFourData_13_6_18 line 442
  23. def OAI.LaughlinFock.collectedFourData_13_6_19 line 450
  24. def OAI.LaughlinFock.collectedFourData_13_6_20 line 462
  25. def OAI.LaughlinFock.collectedFourData_13_6_21 line 479
  26. def OAI.LaughlinFock.collectedFourData_13_6_22 line 502
  27. def OAI.LaughlinFock.collectedFourData_13_6_23 line 532
  28. def OAI.LaughlinFock.collectedFourData_13_6_24 line 570