OAI/Analysis/LaughlinGap/RationalExterior.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Rational Exterior.

  1. def OAI.LaughlinGap.Occupation.wordSign line 15
  2. lemma OAI.LaughlinGap.Occupation.word_empty line 20
  3. lemma OAI.LaughlinGap.Occupation.word_adjoint_vacuum line 33
  4. lemma OAI.LaughlinGap.RealOccupation.limitingPair_roots line 47
  5. abbrev OAI.LaughlinGap.RealOccupation.FourTerm line 58
  6. def OAI.LaughlinGap.RealOccupation.fourTermP line 61
  7. def OAI.LaughlinGap.RealOccupation.fourTermJ line 63
  8. def OAI.LaughlinGap.RealOccupation.fourTermK line 65
  9. def OAI.LaughlinGap.RealOccupation.fourTermX line 67
  10. def OAI.LaughlinGap.RealOccupation.fourTermY line 69
  11. lemma OAI.LaughlinGap.RealOccupation.fourTerm_balance line 71
  12. def OAI.LaughlinGap.RealOccupation.fourTermLabels line 81
  13. def OAI.LaughlinGap.RealOccupation.fourTermCoefficient line 87
  14. lemma OAI.LaughlinGap.RealOccupation.four_pair_normalization line 92