OAI/Analysis/LaughlinGap/ThreeSpin.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Three Spin.

  1. def OAI.LaughlinGap.Spin.onFirstMap line 15
  2. lemma OAI.LaughlinGap.Spin.onFirstMap_apply line 25
  3. lemma OAI.LaughlinGap.Spin.onFirstMap_onSecond line 29
  4. def OAI.LaughlinGap.Spin.LadderMap.tensorRight line 49
  5. def OAI.LaughlinGap.Spin.tripleSpin line 71
  6. def OAI.LaughlinGap.Spin.swap23Linear line 74
  7. def OAI.LaughlinGap.Spin.swap23 line 79
  8. def OAI.LaughlinGap.Spin.pairInclusion line 96
  9. lemma OAI.LaughlinGap.Spin.pairInclusion_apply line 105
  10. def OAI.LaughlinGap.Spin.pairSpectatorInclusion line 116
  11. lemma OAI.LaughlinGap.Spin.pairSpectatorInclusion_apply line 120
  12. def OAI.LaughlinGap.Spin.compressedSwap line 128
  13. def OAI.LaughlinGap.Spin.swapScalar line 132
  14. theorem OAI.LaughlinGap.Spin.compressedSwap_eigenvector line 136