OAI/Analysis/LaughlinGap/ExtendedPair.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Extended Pair.

  1. def OAI.LaughlinGap.Occupation.endCongr line 14
  2. lemma OAI.LaughlinGap.Occupation.endCongr_transition line 17
  3. lemma OAI.LaughlinGap.Occupation.endCongr_adjoint line 20
  4. def OAI.LaughlinGap.Occupation.extendTo line 23
  5. lemma OAI.LaughlinGap.Occupation.endCongr_extendLocal line 27
  6. lemma OAI.LaughlinGap.Occupation.extendTo_add_dim line 32
  7. lemma OAI.LaughlinGap.Occupation.extendTo_annihilation line 36
  8. lemma OAI.LaughlinGap.Occupation.extendTo_adjoint line 43
  9. lemma OAI.LaughlinGap.Occupation.extendTo_matrixLift line 49
  10. lemma OAI.LaughlinGap.Occupation.localPair_support line 54
  11. lemma OAI.LaughlinGap.Occupation.extendTo_localPair line 58
  12. theorem OAI.LaughlinGap.Occupation.local_four_family_transfer_to line 80