OAI/Analysis/LaughlinFock/PairLie.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pair Lie.

  1. theorem OAI.LaughlinFock.wedgeAnnihilator_smul line 12
  2. theorem OAI.LaughlinFock.symmetric_sum_upper line 22
  3. theorem OAI.LaughlinFock.tensorWedge_contraction line 46
  4. theorem OAI.LaughlinFock.tensorWedge_intertwines line 66
  5. def OAI.LaughlinFock.pairSpinMatrix line 76
  6. theorem OAI.LaughlinFock.tensorWedge_pairSpinMatrix line 81
  7. theorem OAI.LaughlinFock.pairSpinMatrix_intertwines line 118