OAI/MathematicalPhysics/Heisenberg/PinnedColors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Heisenberg.Surface.PinnedColor line 13
2. instance OAI.Heisenberg.Surface.(instance at line 15) line 15
3. lemma OAI.Heisenberg.Surface.pinnedColor_sameCycle line 18
4. def OAI.Heisenberg.Surface.pinnedColorEquiv line 22
5. lemma OAI.Heisenberg.Surface.card_pinnedColor line 46
6. def OAI.Heisenberg.Surface.halfSpin line 51
7. lemma OAI.Heisenberg.Surface.sum_halfSpin_bit line 53
8. lemma OAI.Heisenberg.Surface.missing_iff_nohit line 64
9. theorem OAI.Heisenberg.Surface.sum_pinned_spin line 72
10. theorem OAI.Heisenberg.Surface.pinned_trace line 87