OAI/MathematicalPhysics/Heisenberg/SpinField.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.totalZ line 12
2. lemma OAI.Heisenberg.totalZ_selfAdjoint line 14
3. lemma OAI.Heisenberg.finiteRepresentation_totalZ line 18
4. def OAI.Heisenberg.shiftedField line 29
5. lemma OAI.Heisenberg.shiftedField_selfAdjoint line 34
6. lemma OAI.Heisenberg.finiteRepresentation_field line 40
7. lemma OAI.Heisenberg.field_commute line 47
8. lemma OAI.Heisenberg.shiftedField_gibbs_totalZ line 59
9. lemma OAI.Heisenberg.nearestNeighbor_iff_step line 79