OAI/Analysis/Laughlin/Operators/CAR.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Laughlin.Fock.Orbital line 10

    Also declared: ComparatorChallenges/LaughlinPlanar.lean:18 (same declaration text).

  2. abbrev OAI.Laughlin.Fock.Space line 11

    Also declared: ComparatorChallenges/LaughlinPlanar.lean:19 (same declaration text).

  3. def OAI.Laughlin.Fock.mode line 13
  4. def OAI.Laughlin.Fock.create line 15
  5. def OAI.Laughlin.Fock.annihilate line 20

    Also declared: ComparatorChallenges/LaughlinPlanar.lean:21 (same declaration text).

  6. theorem OAI.Laughlin.Fock.annihilate_anticommute line 23
  7. theorem OAI.Laughlin.Fock.create_anticommute line 33
  8. theorem OAI.Laughlin.Fock.mixed_car line 40
  9. theorem OAI.Laughlin.Fock.annihilate_sq line 54
  10. theorem OAI.Laughlin.Fock.create_sq line 59