OAI/Analysis/LaughlinFock/Certificate18.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Certificate18.

  1. theorem OAI.LaughlinFock.fourYLower_18 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_18 line 135
  3. def OAI.LaughlinFock.fourHighestCache_18_0 line 144
  4. def OAI.LaughlinFock.fourHighestCache_18_1 line 151
  5. def OAI.LaughlinFock.fourHighestCache_18_2 line 158
  6. def OAI.LaughlinFock.fourHighestCache_18_3 line 165
  7. def OAI.LaughlinFock.fourHighestCache_18_4 line 172
  8. def OAI.LaughlinFock.fourHighestCache_18_5 line 179
  9. def OAI.LaughlinFock.fourHighestCache_18_6 line 186
  10. def OAI.LaughlinFock.fourHighestCache_18_7 line 193
  11. def OAI.LaughlinFock.fourHighestCache_18_8 line 200
  12. def OAI.LaughlinFock.fourHighestCache_18_9 line 207
  13. def OAI.LaughlinFock.fourHighestCache_18 line 213
  14. theorem OAI.LaughlinFock.fourHighestNumber_18_1 line 215
  15. theorem OAI.LaughlinFock.fourHighestNumber_18_3 line 221
  16. theorem OAI.LaughlinFock.fourHighestNumber_18_5 line 227
  17. theorem OAI.LaughlinFock.fourHighestNumber_18_7 line 233
  18. theorem OAI.LaughlinFock.fourHighestNumber_18_9 line 239
  19. theorem OAI.LaughlinFock.fourHighestNumber_18_11 line 245
  20. theorem OAI.LaughlinFock.fourHighestNumber_18_13 line 251
  21. theorem OAI.LaughlinFock.fourHighestNumber_18_15 line 257
  22. theorem OAI.LaughlinFock.fourHighestNumber_18_17 line 263
  23. theorem OAI.LaughlinFock.fourHighestChecked_18 line 269
  24. theorem OAI.LaughlinFock.fourZChecked_18 line 283
  25. theorem OAI.LaughlinFock.fourLDLChecked_18 line 292
  26. theorem OAI.LaughlinFock.fourPivotChecked_18 line 309
  27. theorem OAI.LaughlinFock.integer_certificate_18 line 313