OAI/Analysis/Laughlin/Spin/TensorAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Rotation.tensorMatrix line 10
  2. theorem OAI.Laughlin.Rotation.tensorMatrix_mul line 13
  3. theorem OAI.Laughlin.Rotation.tensorMatrix_one line 19
  4. theorem OAI.Laughlin.Rotation.tensorMatrix_conjTranspose line 29
  5. theorem OAI.Laughlin.Rotation.tensorMatrix_unitary line 34
  6. abbrev OAI.Laughlin.Rotation.SourceSU2 line 43
  7. def OAI.Laughlin.Rotation.sourceTensorRepresentation line 45
  8. theorem OAI.Laughlin.Rotation.sourceTensorRepresentation_unitary line 51