OAI/Analysis/LaughlinFock/FasterTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Faster Trace.

  1. def OAI.LaughlinFock.shortNumericRowTerm line 11
  2. theorem OAI.LaughlinFock.numericRowTerm_short line 20
  3. def OAI.LaughlinFock.directIntegerSum line 26
  4. theorem OAI.LaughlinFock.directIntegerSum_spec line 30
  5. def OAI.LaughlinFock.shortNumericFourTrace line 36
  6. theorem OAI.LaughlinFock.numericFourTrace_short line 40
  7. def OAI.LaughlinFock.shortNumericRowsFourTrace line 44
  8. theorem OAI.LaughlinFock.integerRowsFourTrace_short line 50