OAI/MathematicalPhysics/BFSS/SpinCoupling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Spin-one-half Casimir algebra and invertible shifted tensor couplings.

  1. lemma OAI.BFSSSpinHalf.tensor_mul line 13
  2. lemma OAI.BFSSSpinHalf.coupled_diagonal line 20
  3. lemma OAI.BFSSSpinHalf.coupled_pair line 25
  4. theorem OAI.BFSSSpinHalf.casimir_identity line 36
  5. theorem OAI.BFSSSpinHalf.shift_norm_lower line 67
  6. def OAI.BFSSSpinHalf.eucAlg line 107
  7. lemma OAI.BFSSSpinHalf.eucAlg_eq line 110
  8. lemma OAI.BFSSSpinHalf.transpose_inner line 112
  9. lemma OAI.BFSSSpinHalf.skew_inner line 119
  10. lemma OAI.BFSSSpinHalf.symmetric_inner line 124
  11. theorem OAI.BFSSSpinHalf.matrix_shift_trivial_kernel line 129
  12. lemma OAI.BFSSSpinHalf.skew_matrix_of_inner line 150
  13. def OAI.BFSSSpinHalf.leftLift line 161
  14. def OAI.BFSSSpinHalf.rightLift line 170
  15. lemma OAI.BFSSSpinHalf.lifts_commute line 179
  16. lemma OAI.BFSSSpinHalf.leftLift_transpose line 185
  17. lemma OAI.BFSSSpinHalf.rightLift_transpose line 190