OAI/MathematicalPhysics/Heisenberg/SlotColorTrace.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Heisenberg.SlotColor.Color line 11
2. abbrev OAI.Heisenberg.SlotColor.Cycles line 12
3. def OAI.Heisenberg.SlotColor.cycleOf line 14
4. lemma OAI.Heisenberg.SlotColor.cycleOf_apply line 16
5. def OAI.Heisenberg.SlotColor.permute line 19
6. lemma OAI.Heisenberg.SlotColor.permute_apply line 25
7. lemma OAI.Heisenberg.SlotColor.permute_mul line 28
8. lemma OAI.Heisenberg.SlotColor.permute_fixed line 32
9. def OAI.Heisenberg.SlotColor.matrix line 45
10. lemma OAI.Heisenberg.SlotColor.matrix_one line 48
11. lemma OAI.Heisenberg.SlotColor.matrix_mul line 53
12. def OAI.Heisenberg.SlotColor.representation line 62
13. lemma OAI.Heisenberg.SlotColor.trace_diagonal line 67
14. abbrev OAI.Heisenberg.SlotColor.ClosedColor line 75
15. instance OAI.Heisenberg.SlotColor.(instance at line 76) line 76
16. instance OAI.Heisenberg.SlotColor.(instance at line 77) line 77
17. lemma OAI.Heisenberg.SlotColor.const_cycle line 79
18. def OAI.Heisenberg.SlotColor.cycleColorEquiv line 89
19. theorem OAI.Heisenberg.SlotColor.trace_cycle_colors line 97
20. lemma OAI.Heisenberg.SlotColor.trace_cycle_weight line 108
21. def OAI.Heisenberg.SlotColor.magnetization line 113
22. lemma OAI.Heisenberg.SlotColor.magnetization_bound line 115
23. theorem OAI.Heisenberg.SlotColor.spectral_cycle_law line 125