OAI/Analysis/Laughlin/Operators/WedgePairRepresentation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Spin.real_matrix_inverse_complex line 9
  2. theorem OAI.Laughlin.Spin.real_matrix_adjoint line 17
  3. def OAI.Laughlin.Spin.complexPairBasis line 22
  4. theorem OAI.Laughlin.Spin.complexPairBasis_isometry line 24
  5. theorem OAI.Laughlin.Spin.complexPairBasis_complete line 29
  6. def OAI.Laughlin.Spin.pairBasisAction line 34
  7. theorem OAI.Laughlin.Spin.wedgePairMatrix_basis line 39
  8. theorem OAI.Laughlin.Spin.wedgePairMatrix_factor line 54
  9. theorem OAI.Laughlin.Spin.pairBasisAction_one line 58
  10. theorem OAI.Laughlin.Spin.pairBasisAction_mul line 62
  11. theorem OAI.Laughlin.Spin.wedgePairMatrix_one line 66
  12. theorem OAI.Laughlin.Spin.wedgePairMatrix_mul line 69
  13. def OAI.Laughlin.Spin.wedgePairRepresentation line 79
  14. theorem OAI.Laughlin.Spin.wedgePairRepresentation_continuous line 85
  15. theorem OAI.Laughlin.Spin.wedgePairRepresentation_inv line 92