OAI/Analysis/LaughlinFock/Certificate17.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Certificate17.

  1. theorem OAI.LaughlinFock.fourYLower_17 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_17 line 135
  3. def OAI.LaughlinFock.fourHighestCache_17_0 line 144
  4. def OAI.LaughlinFock.fourHighestCache_17_1 line 151
  5. def OAI.LaughlinFock.fourHighestCache_17_2 line 158
  6. def OAI.LaughlinFock.fourHighestCache_17_3 line 165
  7. def OAI.LaughlinFock.fourHighestCache_17_4 line 172
  8. def OAI.LaughlinFock.fourHighestCache_17_5 line 179
  9. def OAI.LaughlinFock.fourHighestCache_17_6 line 186
  10. def OAI.LaughlinFock.fourHighestCache_17_7 line 193
  11. def OAI.LaughlinFock.fourHighestCache_17_8 line 200
  12. def OAI.LaughlinFock.fourHighestCache_17 line 205
  13. theorem OAI.LaughlinFock.fourHighestNumber_17_1 line 207
  14. theorem OAI.LaughlinFock.fourHighestNumber_17_3 line 213
  15. theorem OAI.LaughlinFock.fourHighestNumber_17_5 line 219
  16. theorem OAI.LaughlinFock.fourHighestNumber_17_7 line 225
  17. theorem OAI.LaughlinFock.fourHighestNumber_17_9 line 231
  18. theorem OAI.LaughlinFock.fourHighestNumber_17_11 line 237
  19. theorem OAI.LaughlinFock.fourHighestNumber_17_13 line 243
  20. theorem OAI.LaughlinFock.fourHighestNumber_17_15 line 249
  21. theorem OAI.LaughlinFock.fourHighestNumber_17_17 line 255
  22. theorem OAI.LaughlinFock.fourHighestChecked_17 line 261
  23. theorem OAI.LaughlinFock.fourZChecked_17 line 275
  24. theorem OAI.LaughlinFock.fourLDLChecked_17 line 284
  25. theorem OAI.LaughlinFock.fourPivotChecked_17 line 301
  26. theorem OAI.LaughlinFock.integer_certificate_17 line 305