OAI/MathematicalPhysics/Heisenberg/SpinTranslations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Heisenberg.hom_ext_localUnit line 11
2. lemma OAI.Heisenberg.translation_add line 21
3. lemma OAI.Heisenberg.translation_zero line 31
4. lemma OAI.Heisenberg.nearestNeighbor_add line 39
5. lemma OAI.Heisenberg.translation_bond line 42
6. lemma OAI.Heisenberg.directed_bond_double_sum line 51
7. lemma OAI.Heisenberg.translation_hamiltonian line 59
8. lemma OAI.Heisenberg.translation_exp line 74
9. lemma OAI.Heisenberg.translation_finiteDynamics line 79