OAI/Analysis/Laughlin/Pair/NormalOrder.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Fock.pairEnd_create_createline 8 - theorem
OAI.Laughlin.Fock.pairEnd_annihilate_commuteline 30 - theorem
OAI.Laughlin.Fock.pairEnd_commuteline 50