OAI/Analysis/LaughlinFock/Certificate16.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Certificate16.

  1. theorem OAI.LaughlinFock.fourYLower_16 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_16 line 110
  3. def OAI.LaughlinFock.fourHighestCache_16_0 line 119
  4. def OAI.LaughlinFock.fourHighestCache_16_1 line 126
  5. def OAI.LaughlinFock.fourHighestCache_16_2 line 133
  6. def OAI.LaughlinFock.fourHighestCache_16_3 line 140
  7. def OAI.LaughlinFock.fourHighestCache_16_4 line 147
  8. def OAI.LaughlinFock.fourHighestCache_16_5 line 154
  9. def OAI.LaughlinFock.fourHighestCache_16_6 line 161
  10. def OAI.LaughlinFock.fourHighestCache_16 line 167
  11. theorem OAI.LaughlinFock.fourHighestNumber_16_1 line 169
  12. theorem OAI.LaughlinFock.fourHighestNumber_16_3 line 175
  13. theorem OAI.LaughlinFock.fourHighestNumber_16_5 line 181
  14. theorem OAI.LaughlinFock.fourHighestNumber_16_7 line 187
  15. theorem OAI.LaughlinFock.fourHighestNumber_16_9 line 193
  16. theorem OAI.LaughlinFock.fourHighestNumber_16_11 line 199
  17. theorem OAI.LaughlinFock.fourHighestNumber_16_13 line 205
  18. theorem OAI.LaughlinFock.fourHighestNumber_16_15 line 211
  19. theorem OAI.LaughlinFock.fourHighestChecked_16 line 217
  20. theorem OAI.LaughlinFock.fourZChecked_16 line 230
  21. theorem OAI.LaughlinFock.fourLDLChecked_16 line 239
  22. theorem OAI.LaughlinFock.fourPivotChecked_16 line 256
  23. theorem OAI.LaughlinFock.integer_certificate_16 line 260