OAI/Analysis/Laughlin/Fock/Quadruple.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Laughlin.Fock.FourOccupationline 9 - def
OAI.Laughlin.Fock.occupationQuadrupleline 12 - theorem
OAI.Laughlin.Fock.occupationQuadruple_injectiveline 20 - def
OAI.Laughlin.Fock.quadrupleEmbeddingline 35