OAI/MathematicalPhysics/BFSS/GammaWords.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Clifford words, trace orthogonality and finite gamma-matrix bases.

  1. abbrev OAI.BFSSGamma.Space line 10
  2. abbrev OAI.BFSSGamma.Spin line 11
  3. abbrev OAI.BFSSGamma.Mat line 12
  4. def OAI.BFSSGamma.gammaTwo line 16
  5. def OAI.BFSSGamma.symm line 17
  6. def OAI.BFSSGamma.SpinIdentity line 19
  7. lemma OAI.BFSSGamma.gamma_sq line 25
  8. lemma OAI.BFSSGamma.gamma_anti line 33
  9. def OAI.BFSSGamma.singleSign line 37
  10. def OAI.BFSSGamma.word line 39
  11. def OAI.BFSSGamma.reverseWord line 41
  12. def OAI.BFSSGamma.wordSign line 43
  13. lemma OAI.BFSSGamma.gamma_conj line 45
  14. lemma OAI.BFSSGamma.conj_mul line 52
  15. lemma OAI.BFSSGamma.list_conj line 59
  16. lemma OAI.BFSSGamma.word_conj line 67
  17. lemma OAI.BFSSGamma.list_inverse line 73
  18. lemma OAI.BFSSGamma.reverseWord_mul_word line 84
  19. lemma OAI.BFSSGamma.trace_conj line 87
  20. lemma OAI.BFSSGamma.wordSign_eq line 91
  21. lemma OAI.BFSSGamma.wordSign_eq_or line 105
  22. lemma OAI.BFSSGamma.signs_separate line 112
  23. lemma OAI.BFSSGamma.reverseWord_conj line 132
  24. lemma OAI.BFSSGamma.trace_reverseWord_word line 142
  25. abbrev OAI.BFSSGamma.ShortIndex line 163
  26. def OAI.BFSSGamma.shortSet line 165
  27. lemma OAI.BFSSGamma.shortSet_card line 168
  28. lemma OAI.BFSSGamma.shortSet_injective line 173
  29. lemma OAI.BFSSGamma.shortIndex_card line 184
  30. lemma OAI.BFSSGamma.words_linearIndependent line 189
  31. lemma OAI.BFSSGamma.words_span line 207
  32. lemma OAI.BFSSGamma.list_commute line 213
  33. def OAI.BFSSGamma.rankSign line 228
  34. lemma OAI.BFSSGamma.list_reverse_eq line 230
  35. lemma OAI.BFSSGamma.list_transpose line 246
  36. lemma OAI.BFSSGamma.word_transpose line 255
  37. lemma OAI.BFSSGamma.symm_transpose line 261
  38. lemma OAI.BFSSGamma.matrix_eq_of_trace_words line 266
  39. lemma OAI.BFSSGamma.sum_word_conj line 281
  40. lemma OAI.BFSSGamma.gammaTwo_alt line 304