OAI/Analysis/LaughlinFock/WedgeLie.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Wedge Lie.

  1. theorem OAI.LaughlinFock.wedgeAnnihilator_neg line 12
  2. theorem OAI.LaughlinFock.oneBody_wedgeAnnihilator_commutator_skew line 18
  3. theorem OAI.LaughlinFock.sector_intertwiner_of_commutators line 31
  4. theorem OAI.LaughlinFock.wedge_intertwiner_commutator line 49
  5. def OAI.LaughlinFock.tensorSum line 62
  6. theorem OAI.LaughlinFock.tensorSum_apply line 66
  7. def OAI.LaughlinFock.wedgeProductMatrix line 77
  8. theorem OAI.LaughlinFock.wedgeProductMatrix_contraction line 84
  9. theorem OAI.LaughlinFock.wedgeProductMatrix_intertwines line 95
  10. def OAI.LaughlinFock.oneParticleMatrix line 120
  11. theorem OAI.LaughlinFock.oneParticleMatrix_contraction line 123
  12. theorem OAI.LaughlinFock.oneParticleMatrix_intertwines line 131