OAI/Analysis/LaughlinFock/CoupledLie.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Coupled Lie.

  1. theorem OAI.LaughlinFock.spinLower_sum line 11
  2. theorem OAI.LaughlinFock.spinRaise_sum line 26
  3. theorem OAI.LaughlinFock.sum_spinLower line 42
  4. theorem OAI.LaughlinFock.sum_spinRaise line 50
  5. theorem OAI.LaughlinFock.tensorSum_mul_apply line 58
  6. def OAI.LaughlinFock.coupledSpinMatrix line 74
  7. theorem OAI.LaughlinFock.tensorLower_coupled_apply line 78
  8. theorem OAI.LaughlinFock.tensorRaise_coupled_apply line 92
  9. theorem OAI.LaughlinFock.coupledSpinMatrix_lower line 105
  10. theorem OAI.LaughlinFock.coupledSpinMatrix_raise line 114
  11. theorem OAI.LaughlinFock.coupledSpinMatrix_weight line 123
  12. theorem OAI.LaughlinFock.tensorSum_add line 139
  13. theorem OAI.LaughlinFock.tensorSum_smul line 146
  14. theorem OAI.LaughlinFock.tensorSum_sub line 153
  15. theorem OAI.LaughlinFock.coupledSpinMatrix_intertwines line 161