OAI/Analysis/LaughlinFock/RationalWedge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Rational Wedge.

  1. def OAI.LaughlinFock.rationalWordVacuum line 12
  2. theorem OAI.LaughlinFock.annihilatorList_vacuum_rational line 17
  3. theorem OAI.LaughlinFock.rationalWordVacuum_support line 27
  4. def OAI.LaughlinFock.occupationFactorial line 43
  5. def OAI.LaughlinFock.factorialMode line 46
  6. theorem OAI.LaughlinFock.factorialMode_ne_zero line 49
  7. def OAI.LaughlinFock.rationalHighestTerm line 53
  8. theorem OAI.LaughlinFock.copy_pair_factorial line 59
  9. def OAI.LaughlinFock.rationalHighestEntry line 97
  10. theorem OAI.LaughlinFock.factorial_conjugate_highest line 103
  11. theorem OAI.LaughlinFock.occupationFactorial_pos line 151
  12. theorem OAI.LaughlinFock.factorialMode_prod line 156
  13. theorem OAI.LaughlinFock.planarFourWedgeMatrix_rational line 162
  14. def OAI.LaughlinFock.rationalFourGram line 197
  15. theorem OAI.LaughlinFock.planarFourGram_rational line 202