OAI/MathematicalPhysics/BFSS/NormalFields.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Normal linear fields, Clifford kinetic symbols and potential identities.

  1. def OAI.BFSSQuantum.AlgebraData.normalLinearField line 22
  2. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_apply line 26
  3. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_difference line 31
  4. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_selfAdjoint line 38
  5. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_anticommutator line 54
  6. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_zero line 63
  7. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_scaled line 78
  8. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_potential_average line 91
  9. lemma OAI.BFSSSliceAnalytic.contraction_projection line 130
  10. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_eq_zero line 158
  11. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_projection line 171
  12. lemma OAI.BFSSQuantum.AlgebraData.kineticSkewLinear_skew line 186
  13. lemma OAI.BFSSQuantum.AlgebraData.normalLinearField_anticommutator_linear line 197
  14. abbrev OAI.BFSSQuantum.AlgebraData.NormalIndex line 216
  15. def OAI.BFSSQuantum.AlgebraData.normalBasisVector line 218
  16. def OAI.BFSSQuantum.AlgebraData.normalKineticSymbol line 221
  17. def OAI.BFSSQuantum.AlgebraData.normalKineticSkewSymbol line 225
  18. lemma OAI.BFSSQuantum.AlgebraData.normalKineticSymbol_selfAdjoint line 228
  19. lemma OAI.BFSSQuantum.AlgebraData.normalKineticSymbol_CAR line 237
  20. lemma OAI.BFSSQuantum.AlgebraData.normalFermion_contraction line 251