OAI/MathematicalPhysics/Heisenberg/SpinMatrixTrace.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Heisenberg.realFunctionalline 12 - lemma
OAI.Heisenberg.finiteRepresentation_traceline 15 - lemma
OAI.Heisenberg.finiteRepresentation_expline 31 - lemma
OAI.Heisenberg.finiteRepresentation_gibbsDensityline 37 - lemma
OAI.Heisenberg.finiteRepresentation_gibbs_reline 44