OAI/Analysis/LaughlinFock/Sparse1308.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Sparse1308.

  1. def OAI.LaughlinFock.collectedFourData_13_3_51 line 9
  2. def OAI.LaughlinFock.collectedFourData_13_3_52 line 30
  3. def OAI.LaughlinFock.collectedFourData_13_3_53 line 59
  4. def OAI.LaughlinFock.collectedFourData_13_3_54 line 96
  5. def OAI.LaughlinFock.collectedFourData_13_3_55 line 140
  6. def OAI.LaughlinFock.collectedFourData_13_3 line 190
  7. theorem OAI.LaughlinFock.collectedFourChecked_13_3 line 249
  8. def OAI.LaughlinFock.collectedFourData_13_4_0 line 252
  9. def OAI.LaughlinFock.collectedFourData_13_4_1 line 256
  10. def OAI.LaughlinFock.collectedFourData_13_4_2 line 263
  11. def OAI.LaughlinFock.collectedFourData_13_4_3 line 275
  12. def OAI.LaughlinFock.collectedFourData_13_4_4 line 293
  13. def OAI.LaughlinFock.collectedFourData_13_4_5 line 318
  14. def OAI.LaughlinFock.collectedFourData_13_4_6 line 322
  15. def OAI.LaughlinFock.collectedFourData_13_4_7 line 329
  16. def OAI.LaughlinFock.collectedFourData_13_4_8 line 341
  17. def OAI.LaughlinFock.collectedFourData_13_4_9 line 359
  18. def OAI.LaughlinFock.collectedFourData_13_4_10 line 384
  19. def OAI.LaughlinFock.collectedFourData_13_4_11 line 417
  20. def OAI.LaughlinFock.collectedFourData_13_4_12 line 421
  21. def OAI.LaughlinFock.collectedFourData_13_4_13 line 428
  22. def OAI.LaughlinFock.collectedFourData_13_4_14 line 440
  23. def OAI.LaughlinFock.collectedFourData_13_4_15 line 458
  24. def OAI.LaughlinFock.collectedFourData_13_4_16 line 483
  25. def OAI.LaughlinFock.collectedFourData_13_4_17 line 516
  26. def OAI.LaughlinFock.collectedFourData_13_4_18 line 557
  27. def OAI.LaughlinFock.collectedFourData_13_4_19 line 561
  28. def OAI.LaughlinFock.collectedFourData_13_4_20 line 568
  29. def OAI.LaughlinFock.collectedFourData_13_4_21 line 580
  30. def OAI.LaughlinFock.collectedFourData_13_4_22 line 598