OAI/Analysis/LaughlinFock/SpinSchur.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Spin Schur.

  1. theorem OAI.LaughlinFock.matrix_commutes_generator_of_flow line 17
  2. theorem OAI.LaughlinFock.rotationAverage_commutes_generator line 34
  3. def OAI.LaughlinFock.spinLowerMatrix line 48
  4. def OAI.LaughlinFock.spinWeightMatrix line 52
  5. def OAI.LaughlinFock.spinGenerator line 56
  6. theorem OAI.LaughlinFock.spinWeightMatrix_adjoint line 61
  7. theorem OAI.LaughlinFock.spinGenerator_skew line 64
  8. theorem OAI.LaughlinFock.spinGenerator_intertwiner line 71
  9. theorem OAI.LaughlinFock.mul_spinLower_succ line 106
  10. theorem OAI.LaughlinFock.mul_spinRaise_zero line 120
  11. theorem OAI.LaughlinFock.spinRaise_mul_pred line 126
  12. theorem OAI.LaughlinFock.spin_intertwiner_zero_of_first_column line 141
  13. theorem OAI.LaughlinFock.spin_intertwiner_first_column line 162
  14. theorem OAI.LaughlinFock.spin_intertwiner_scalar line 174
  15. theorem OAI.LaughlinFock.spin_intertwiner_zero_of_ne line 193
  16. theorem OAI.LaughlinFock.spin_intertwiner_trace_scalar line 211