OAI/Analysis/LaughlinGap/RealSpinSquare.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Real Spin Square.

  1. lemma OAI.LaughlinGap.matrixLift_reindex line 14
  2. lemma OAI.LaughlinGap.RealOccupation.complexify_physicalTriple line 29
  3. lemma OAI.LaughlinGap.RealOccupation.complexify_three_lift line 33
  4. lemma OAI.LaughlinGap.RealOccupation.physicalThreeProjection_real line 53
  5. lemma OAI.LaughlinGap.RealOccupation.complexify_threeSpinLift line 61
  6. lemma OAI.LaughlinGap.RealOccupation.threeSpinLift_null line 66
  7. def OAI.LaughlinGap.RealOccupation.fourTarget line 72
  8. lemma OAI.LaughlinGap.RealOccupation.fourTarget_positive line 77
  9. lemma OAI.LaughlinGap.RealOccupation.complexify_fourTarget line 80
  10. theorem OAI.LaughlinGap.RealOccupation.physical_spin_square_real line 86