OAI/Analysis/LaughlinGap/CovariantLift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Covariant Lift.

  1. def OAI.LaughlinGap.RealOccupation.lift line 17
  2. def OAI.LaughlinGap.RealOccupation.combination line 23
  3. lemma OAI.LaughlinGap.RealOccupation.lift_rankOne line 30
  4. lemma OAI.LaughlinGap.RealOccupation.lift_transpose line 39
  5. lemma OAI.LaughlinGap.RealOccupation.lift_positive line 47
  6. lemma OAI.LaughlinGap.RealOccupation.complexify_combination line 62
  7. lemma OAI.LaughlinGap.RealOccupation.complexify_lift line 70
  8. structure OAI.LaughlinGap.RealOccupation.Covariant line 76
  9. lemma OAI.LaughlinGap.RealOccupation.commutator_transpose line 81
  10. lemma OAI.LaughlinGap.RealOccupation.Covariant.transpose line 88
  11. lemma OAI.LaughlinGap.RealOccupation.Covariant.commutator_lift line 94
  12. theorem OAI.LaughlinGap.RealOccupation.Covariant.average_lift line 125
  13. theorem OAI.LaughlinGap.RealOccupation.annihilation_covariant line 132