OAI/Analysis/LaughlinGap/LowNested.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Low Nested.

  1. abbrev OAI.LaughlinGap.Spin.LowNestedIndex line 15
  2. lemma OAI.LaughlinGap.Spin.lowNested_valid line 17
  3. def OAI.LaughlinGap.Spin.lowNestedInclusion line 22
  4. lemma OAI.LaughlinGap.Spin.lowNestedInclusion_injective line 30
  5. lemma OAI.LaughlinGap.Spin.lowNested_coefficient line 45
  6. lemma OAI.LaughlinGap.Spin.nestedTensor_low_expansion line 82