OAI/Analysis/Laughlin/FourBody/PairTarget.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Fock.pairCoupledOne_contractline 10 - theorem
OAI.Laughlin.Fock.fourPairEmbedding_contractline 45 - theorem
OAI.Laughlin.Fock.contractionForm_factor_oneline 56 - theorem
OAI.Laughlin.Fock.fourPairTargetMatrix_Fockline 66 - theorem
OAI.Laughlin.Fock.sourceA4Form_boundline 83