OAI/Analysis/LaughlinGap/RationalCreatedGram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational Created Gram.

  1. lemma OAI.LaughlinGap.Occupation.wordSign_ne_zero_nodup line 14
  2. def OAI.LaughlinGap.RealOccupation.rootSetWeight line 28
  3. def OAI.LaughlinGap.RealOccupation.setFactorial line 31
  4. lemma OAI.LaughlinGap.RealOccupation.rootSetWeight_sq line 33
  5. lemma OAI.LaughlinGap.RealOccupation.rootSetWeight_ne_zero line 37
  6. def OAI.LaughlinGap.RealOccupation.fourColumn line 40
  7. def OAI.LaughlinGap.RealOccupation.fourKeys line 44
  8. lemma OAI.LaughlinGap.RealOccupation.fourColumn_support line 48
  9. lemma OAI.LaughlinGap.RealOccupation.four_term_denominator line 60
  10. lemma OAI.LaughlinGap.RealOccupation.four_created_column line 76
  11. def OAI.LaughlinGap.RealOccupation.rationalCreatedGram line 99
  12. lemma OAI.LaughlinGap.RealOccupation.createdGram_rational line 102