OAI/MathematicalPhysics/BFSS/FrequencyContraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Kinetic-mass and color contractions for the literal fermion field.

  1. lemma OAI.BFSSQuantum.AlgebraData.kineticComplexSymbol_sum line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.kinetic_matrix_contraction line 28
  3. lemma OAI.BFSSQuantum.AlgebraData.gamma_mass_contraction line 50
  4. lemma OAI.BFSSQuantum.AlgebraData.massLinear_single line 64
  5. lemma OAI.BFSSQuantum.AlgebraData.kinetic_mass_contraction line 93
  6. lemma OAI.BFSSQuantum.AlgebraData.deformedFermionField_mass line 116
  7. def OAI.BFSSQuantum.AlgebraData.spinColumn line 192
  8. lemma OAI.BFSSQuantum.AlgebraData.sum_rotate_five line 195
  9. lemma OAI.BFSSQuantum.AlgebraData.bracketBilinear_restrict line 210
  10. lemma OAI.BFSSQuantum.AlgebraData.structureConstant_cycle line 242
  11. lemma OAI.BFSSQuantum.AlgebraData.structureConstant_swap line 250