OAI/Analysis/LaughlinFock/Certificate15.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Certificate15.

  1. theorem OAI.LaughlinFock.fourYLower_15 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_15 line 110
  3. def OAI.LaughlinFock.fourHighestCache_15_0 line 119
  4. def OAI.LaughlinFock.fourHighestCache_15_1 line 126
  5. def OAI.LaughlinFock.fourHighestCache_15_2 line 133
  6. def OAI.LaughlinFock.fourHighestCache_15_3 line 140
  7. def OAI.LaughlinFock.fourHighestCache_15_4 line 147
  8. def OAI.LaughlinFock.fourHighestCache_15_5 line 154
  9. def OAI.LaughlinFock.fourHighestCache_15 line 160
  10. theorem OAI.LaughlinFock.fourHighestNumber_15_1 line 162
  11. theorem OAI.LaughlinFock.fourHighestNumber_15_3 line 168
  12. theorem OAI.LaughlinFock.fourHighestNumber_15_5 line 174
  13. theorem OAI.LaughlinFock.fourHighestNumber_15_7 line 180
  14. theorem OAI.LaughlinFock.fourHighestNumber_15_9 line 186
  15. theorem OAI.LaughlinFock.fourHighestNumber_15_11 line 192
  16. theorem OAI.LaughlinFock.fourHighestNumber_15_13 line 198
  17. theorem OAI.LaughlinFock.fourHighestNumber_15_15 line 204
  18. theorem OAI.LaughlinFock.fourHighestChecked_15 line 210
  19. theorem OAI.LaughlinFock.fourZChecked_15 line 223
  20. theorem OAI.LaughlinFock.fourLDLChecked_15 line 232
  21. theorem OAI.LaughlinFock.fourPivotChecked_15 line 249
  22. theorem OAI.LaughlinFock.integer_certificate_15 line 253