OAI/Analysis/LaughlinFock/FourBasis.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Four Basis.

  1. theorem OAI.LaughlinFock.wedgeCoupledCoefficient_resolution line 14
  2. def OAI.LaughlinFock.fullCouplingMatrix line 66
  3. theorem OAI.LaughlinFock.fullCouplingMatrix_complete line 70
  4. def OAI.LaughlinFock.oddPairColumns line 81
  5. theorem OAI.LaughlinFock.oddPairColumns_complete line 86
  6. def OAI.LaughlinFock.fourFactorEmbedding line 97
  7. def OAI.LaughlinFock.composedCouplingMatrix line 102
  8. theorem OAI.LaughlinFock.composedCouplingMatrix_eq_product line 106
  9. theorem OAI.LaughlinFock.composedCouplingMatrix_complete line 123