OAI/Analysis/LaughlinFock/Certificate21.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Certificate21.

  1. theorem OAI.LaughlinFock.fourYLower_21 line 13
  2. theorem OAI.LaughlinFock.fourYChecked_21 line 194
  3. def OAI.LaughlinFock.fourHighestCache_21_0 line 203
  4. def OAI.LaughlinFock.fourHighestCache_21_1 line 210
  5. def OAI.LaughlinFock.fourHighestCache_21_2 line 217
  6. def OAI.LaughlinFock.fourHighestCache_21_3 line 224
  7. def OAI.LaughlinFock.fourHighestCache_21_4 line 231
  8. def OAI.LaughlinFock.fourHighestCache_21_5 line 238
  9. def OAI.LaughlinFock.fourHighestCache_21_6 line 245
  10. def OAI.LaughlinFock.fourHighestCache_21_7 line 252
  11. def OAI.LaughlinFock.fourHighestCache_21_8 line 259
  12. def OAI.LaughlinFock.fourHighestCache_21_9 line 266
  13. def OAI.LaughlinFock.fourHighestCache_21_10 line 273
  14. def OAI.LaughlinFock.fourHighestCache_21_11 line 280
  15. def OAI.LaughlinFock.fourHighestCache_21_12 line 287
  16. def OAI.LaughlinFock.fourHighestCache_21_13 line 294
  17. def OAI.LaughlinFock.fourHighestCache_21_14 line 301
  18. def OAI.LaughlinFock.fourHighestCache_21_15 line 308
  19. def OAI.LaughlinFock.fourHighestCache_21 line 315
  20. theorem OAI.LaughlinFock.fourHighestNumber_21_1 line 317
  21. theorem OAI.LaughlinFock.fourHighestNumber_21_3 line 323
  22. theorem OAI.LaughlinFock.fourHighestNumber_21_5 line 329
  23. theorem OAI.LaughlinFock.fourHighestNumber_21_7 line 335
  24. theorem OAI.LaughlinFock.fourHighestNumber_21_9 line 341
  25. theorem OAI.LaughlinFock.fourHighestNumber_21_11 line 347
  26. theorem OAI.LaughlinFock.fourHighestNumber_21_13 line 353
  27. theorem OAI.LaughlinFock.fourHighestNumber_21_15 line 359
  28. theorem OAI.LaughlinFock.fourHighestNumber_21_17 line 365
  29. theorem OAI.LaughlinFock.fourHighestNumber_21_19 line 371
  30. theorem OAI.LaughlinFock.fourHighestNumber_21_21 line 377
  31. theorem OAI.LaughlinFock.fourHighestChecked_21 line 383
  32. theorem OAI.LaughlinFock.fourZChecked_21 line 399
  33. theorem OAI.LaughlinFock.fourLDLChecked_21 line 408
  34. theorem OAI.LaughlinFock.fourPivotChecked_21 line 425
  35. theorem OAI.LaughlinFock.integer_certificate_21 line 429