OAI/Analysis/Laughlin/Exterior/PairConjugation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Fock.pairEnd line 8
  2. def OAI.Laughlin.Fock.sourcePairEnd line 11
  3. def OAI.Laughlin.Fock.limitPairEnd line 14
  4. def OAI.Laughlin.Fock.physicalScaling line 17
  5. def OAI.Laughlin.Fock.physicalScalingInv line 20
  6. theorem OAI.Laughlin.Fock.pairEnd_smul line 23
  7. theorem OAI.Laughlin.Fock.pairEnd_scaling line 27
  8. theorem OAI.Laughlin.Fock.sourcePair_intertwining line 40
  9. theorem OAI.Laughlin.Fock.physicalScaling_left_inverse line 54
  10. theorem OAI.Laughlin.Fock.sourcePair_conjugation line 60