OAI/Analysis/Laughlin/Spin/GeneralSpinAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Rotation.generalSpinMatrix line 9
  2. theorem OAI.Laughlin.Rotation.general_tensor_spin_intertwining line 13
  3. theorem OAI.Laughlin.Rotation.generalSpinMatrix_mul line 28
  4. theorem OAI.Laughlin.Rotation.generalSpinMatrix_one line 39
  5. theorem OAI.Laughlin.Rotation.generalSpinMatrix_source line 42
  6. theorem OAI.Laughlin.Rotation.generalSpinMatrix_diagonal line 45
  7. theorem OAI.Laughlin.Rotation.generalSpinMatrix_transpose line 53
  8. theorem OAI.Laughlin.Rotation.generalSpinMatrix_polynomial line 62