OAI/Analysis/Laughlin/Fock/LaughlinGap.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Laughlin.HaldaneKernelInputline 10 - def
OAI.Laughlin.SharpMainTargetline 14 - theorem
OAI.Laughlin.sharpMainTarget_of_haldaneline 19