OAI/MathematicalPhysics/Heisenberg/SpinMatrixConservation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Heisenberg.TensorMatrix.compress_eq line 11
2. lemma OAI.Heisenberg.TensorMatrix.compress_symmetric line 15
3. lemma OAI.Heisenberg.TensorMatrix.compress_commute line 20
4. lemma OAI.Heisenberg.SlotColor.magnetization_permute line 30
5. lemma OAI.Heisenberg.SlotColor.matrix_mag_commute line 33
6. lemma OAI.Heisenberg.SlotColor.matrix_swap_transpose line 41
7. lemma OAI.Heisenberg.SlotTensor.clockGenerator_transpose line 54
8. lemma OAI.Heisenberg.SlotTensor.clockGenerator_mag line 58
9. lemma OAI.Heisenberg.SlotTensor.spinGenerator_transpose line 77
10. lemma OAI.Heisenberg.SlotTensor.spinGenerator_mag line 82
11. lemma OAI.Heisenberg.SlotTensor.physicalMagnetization_bounds line 93