OAI/Analysis/LaughlinFock/Sparse1404.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Sparse1404.

  1. def OAI.LaughlinFock.collectedFourData_14_2_37 line 8
  2. def OAI.LaughlinFock.collectedFourData_14_2_38 line 40
  3. def OAI.LaughlinFock.collectedFourData_14_2_39 line 79
  4. def OAI.LaughlinFock.collectedFourData_14_2_40 line 83
  5. def OAI.LaughlinFock.collectedFourData_14_2_41 line 92
  6. def OAI.LaughlinFock.collectedFourData_14_2_42 line 108
  7. def OAI.LaughlinFock.collectedFourData_14_2_43 line 132
  8. def OAI.LaughlinFock.collectedFourData_14_2_44 line 164
  9. def OAI.LaughlinFock.collectedFourData_14_2_45 line 203
  10. def OAI.LaughlinFock.collectedFourData_14_2_46 line 212
  11. def OAI.LaughlinFock.collectedFourData_14_2_47 line 228
  12. def OAI.LaughlinFock.collectedFourData_14_2_48 line 252
  13. def OAI.LaughlinFock.collectedFourData_14_2_49 line 284
  14. def OAI.LaughlinFock.collectedFourData_14_2_50 line 323
  15. def OAI.LaughlinFock.collectedFourData_14_2_51 line 339
  16. def OAI.LaughlinFock.collectedFourData_14_2_52 line 363
  17. def OAI.LaughlinFock.collectedFourData_14_2_53 line 395
  18. def OAI.LaughlinFock.collectedFourData_14_2 line 434
  19. theorem OAI.LaughlinFock.collectedFourChecked_14_2 line 491
  20. def OAI.LaughlinFock.collectedFourData_14_3_0 line 494
  21. def OAI.LaughlinFock.collectedFourData_14_3_1 line 498
  22. def OAI.LaughlinFock.collectedFourData_14_3_2 line 502
  23. def OAI.LaughlinFock.collectedFourData_14_3_3 line 506
  24. def OAI.LaughlinFock.collectedFourData_14_3_4 line 514
  25. def OAI.LaughlinFock.collectedFourData_14_3_5 line 528
  26. def OAI.LaughlinFock.collectedFourData_14_3_6 line 549
  27. def OAI.LaughlinFock.collectedFourData_14_3_7 line 553
  28. def OAI.LaughlinFock.collectedFourData_14_3_8 line 557
  29. def OAI.LaughlinFock.collectedFourData_14_3_9 line 561
  30. def OAI.LaughlinFock.collectedFourData_14_3_10 line 569
  31. def OAI.LaughlinFock.collectedFourData_14_3_11 line 583
  32. def OAI.LaughlinFock.collectedFourData_14_3_12 line 604