OAI/Analysis/Laughlin/Exterior/Scaling.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Fock.contraction_mapline 8 - def
OAI.Laughlin.Fock.orbitalScalingline 21 - def
OAI.Laughlin.Fock.exteriorScalingline 26 - theorem
OAI.Laughlin.Fock.projection_scalingline 29 - theorem
OAI.Laughlin.Fock.annihilate_scalingline 34 - theorem
OAI.Laughlin.Fock.exteriorScaling_inverseline 39 - theorem
OAI.Laughlin.Fock.modeFactor_posline 52