OAI/Analysis/LaughlinFock/Certificate19.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Certificate19.

  1. theorem OAI.LaughlinFock.fourYLower_19 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_19 line 163
  3. def OAI.LaughlinFock.fourHighestCache_19_0 line 172
  4. def OAI.LaughlinFock.fourHighestCache_19_1 line 179
  5. def OAI.LaughlinFock.fourHighestCache_19_2 line 186
  6. def OAI.LaughlinFock.fourHighestCache_19_3 line 193
  7. def OAI.LaughlinFock.fourHighestCache_19_4 line 200
  8. def OAI.LaughlinFock.fourHighestCache_19_5 line 207
  9. def OAI.LaughlinFock.fourHighestCache_19_6 line 214
  10. def OAI.LaughlinFock.fourHighestCache_19_7 line 221
  11. def OAI.LaughlinFock.fourHighestCache_19_8 line 228
  12. def OAI.LaughlinFock.fourHighestCache_19_9 line 235
  13. def OAI.LaughlinFock.fourHighestCache_19_10 line 242
  14. def OAI.LaughlinFock.fourHighestCache_19_11 line 249
  15. def OAI.LaughlinFock.fourHighestCache_19 line 255
  16. theorem OAI.LaughlinFock.fourHighestNumber_19_1 line 257
  17. theorem OAI.LaughlinFock.fourHighestNumber_19_3 line 263
  18. theorem OAI.LaughlinFock.fourHighestNumber_19_5 line 269
  19. theorem OAI.LaughlinFock.fourHighestNumber_19_7 line 275
  20. theorem OAI.LaughlinFock.fourHighestNumber_19_9 line 281
  21. theorem OAI.LaughlinFock.fourHighestNumber_19_11 line 287
  22. theorem OAI.LaughlinFock.fourHighestNumber_19_13 line 293
  23. theorem OAI.LaughlinFock.fourHighestNumber_19_15 line 299
  24. theorem OAI.LaughlinFock.fourHighestNumber_19_17 line 305
  25. theorem OAI.LaughlinFock.fourHighestNumber_19_19 line 311
  26. theorem OAI.LaughlinFock.fourHighestChecked_19 line 317
  27. theorem OAI.LaughlinFock.fourZChecked_19 line 332
  28. theorem OAI.LaughlinFock.fourLDLChecked_19 line 341
  29. theorem OAI.LaughlinFock.fourPivotChecked_19 line 358
  30. theorem OAI.LaughlinFock.integer_certificate_19 line 362