OAI/Analysis/LaughlinFock/IntegerFour.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Integer Four.

  1. def OAI.LaughlinFock.integerCopyPolynomial line 13
  2. theorem OAI.LaughlinFock.rationalCopyPolynomial_integer line 18
  3. def OAI.LaughlinFock.integerFourTrace line 23
  4. theorem OAI.LaughlinFock.rationalFourTrace_integer line 31
  5. def OAI.LaughlinFock.integerRowsFourTrace line 36
  6. def OAI.LaughlinFock.integerHighestTerm line 39
  7. theorem OAI.LaughlinFock.fastHighestTerm_integer line 47
  8. def OAI.LaughlinFock.integerHighestEntry line 59
  9. def OAI.LaughlinFock.integerFourGram line 62
  10. theorem OAI.LaughlinFock.rationalFourGram_integer line 67
  11. def OAI.LaughlinFock.integerFourMiddle line 75
  12. def OAI.LaughlinFock.integerCompression line 81