OAI/Analysis/LaughlinGap/NestedSpin.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Nested Spin.

  1. def OAI.LaughlinGap.Spin.onSecondMap line 14
  2. lemma OAI.LaughlinGap.Spin.onSecondMap_apply line 24
  3. lemma OAI.LaughlinGap.Spin.onSecondMap_onFirst line 28
  4. def OAI.LaughlinGap.Spin.LadderMap.tensorLeft line 48
  5. def OAI.LaughlinGap.Spin.nestedSpin line 70
  6. def OAI.LaughlinGap.Spin.nestedEmbedding line 73
  7. def OAI.LaughlinGap.Spin.nestedTensor line 78
  8. lemma OAI.LaughlinGap.Spin.nestedEmbedding_apply line 83
  9. abbrev OAI.LaughlinGap.Spin.NestedIndex line 99
  10. def OAI.LaughlinGap.Spin.nestedFamily line 102
  11. lemma OAI.LaughlinGap.Spin.coupled_tensor_second_dot line 106
  12. lemma OAI.LaughlinGap.Spin.nestedTensor_as_map line 142
  13. lemma OAI.LaughlinGap.Spin.nestedTensor_dot line 148
  14. lemma OAI.LaughlinGap.Spin.nestedFamily_orthonormal line 166
  15. lemma OAI.LaughlinGap.Spin.nestedIndex_card line 172
  16. def OAI.LaughlinGap.Spin.nestedBasis line 184
  17. lemma OAI.LaughlinGap.Spin.nestedBasis_apply line 194
  18. lemma OAI.LaughlinGap.Spin.nestedTensor_expansion line 197