OAI/Analysis/LaughlinGap/IntegerFourRows.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Integer Four Rows.

  1. def OAI.LaughlinGap.Spin.uInt line 15
  2. lemma OAI.LaughlinGap.Spin.uFast_eq_int line 19
  3. def OAI.LaughlinGap.RealOccupation.vInt line 27
  4. lemma OAI.LaughlinGap.RealOccupation.vFast_eq_int line 31
  5. def OAI.LaughlinGap.RealOccupation.fourSumInteger line 34
  6. lemma OAI.LaughlinGap.RealOccupation.fourSumEval_eq_integer line 40
  7. def OAI.LaughlinGap.RealOccupation.fourRowWeight line 50
  8. def OAI.LaughlinGap.RealOccupation.fourMatrixDenominator line 56
  9. lemma OAI.LaughlinGap.RealOccupation.fourRowWeight_eq line 58
  10. def OAI.LaughlinGap.RealOccupation.exactFourInteger line 82
  11. def OAI.LaughlinGap.RealOccupation.exactFourEval line 86
  12. lemma OAI.LaughlinGap.RealOccupation.exactFourEval_eq line 88