OAI/Analysis/Laughlin/Pair/SpinorCube.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Laughlin.pairSpinorPolynomialline 10 - theorem
OAI.Laughlin.pairSpinorPolynomial_homogeneousEvalline 16 - theorem
OAI.Laughlin.pairSpinorPolynomial_cubeline 31 - theorem
OAI.Laughlin.pairSpinorPolynomial_bracket_cubeline 46