OAI/MathematicalPhysics/BFSS/GammaIdentity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The spin identity from trace pairings with Clifford words.

  1. lemma OAI.BFSSGamma.dot_mulVec_left line 17
  2. lemma OAI.BFSSGamma.dot_transpose line 22
  3. lemma OAI.BFSSGamma.trace_mul_outer line 27
  4. lemma OAI.BFSSGamma.trace_symm_outer line 32
  5. lemma OAI.BFSSGamma.trace_skew_symm line 42
  6. def OAI.BFSSGamma.spinLHS line 48
  7. lemma OAI.BFSSGamma.spinLHS_symmetric line 52
  8. lemma OAI.BFSSGamma.spin_trace_pair line 55
  9. lemma OAI.BFSSGamma.trace_word line 87
  10. lemma OAI.BFSSGamma.word_singleton line 93
  11. lemma OAI.BFSSGamma.trace_word_gamma line 99
  12. def OAI.BFSSGamma.spinRHS line 106
  13. lemma OAI.BFSSGamma.spinRHS_symmetric line 110
  14. lemma OAI.BFSSGamma.trace_spinRHS line 115
  15. lemma OAI.BFSSGamma.dot_skew_zero line 123
  16. lemma OAI.BFSSGamma.dot_gamma_product line 129
  17. lemma OAI.BFSSGamma.trace_gamma line 139
  18. lemma OAI.BFSSGamma.spin_identity_trace_word line 143
  19. theorem OAI.BFSSGamma.spinIdentity line 197