OAI/Analysis/LaughlinFock/ThreeCertificate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Three Certificate.

  1. def OAI.LaughlinFock.integerThreeTrace line 12
  2. theorem OAI.LaughlinFock.rationalThreeTrace_integer line 20
  3. def OAI.LaughlinFock.integerRowsThreeTrace line 24
  4. theorem OAI.LaughlinFock.planarRowsThreeTrace_integer line 27
  5. theorem OAI.LaughlinFock.certificate_three_2 line 36
  6. theorem OAI.LaughlinFock.certificate_three_4 line 40
  7. theorem OAI.LaughlinFock.certificate_three_5 line 44
  8. theorem OAI.LaughlinFock.certificate_three_6 line 48
  9. theorem OAI.LaughlinFock.certificate_three_7 line 52
  10. theorem OAI.LaughlinFock.certificate_three_8 line 56
  11. theorem OAI.LaughlinFock.certificate_three_9 line 60
  12. theorem OAI.LaughlinFock.certificate_three_10 line 64
  13. theorem OAI.LaughlinFock.certificate_three_11 line 68
  14. theorem OAI.LaughlinFock.certificate_three_12 line 72
  15. theorem OAI.LaughlinFock.certificate_three_13 line 76
  16. theorem OAI.LaughlinFock.certificate_three_14 line 80
  17. theorem OAI.LaughlinFock.certificate_three_15 line 84
  18. theorem OAI.LaughlinFock.certificate_three line 88