OAI/Analysis/Laughlin/Fock/Bidegree.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Fock.occupation_emptyline 8 - def
OAI.Laughlin.Fock.OccupationBidegreeline 14Also declared: ComparatorChallenges/LaughlinPlanar.lean:28 (same declaration text).
- theorem
OAI.Laughlin.Fock.vacuum_bidegreeline 18 - theorem
OAI.Laughlin.Fock.create_bidegreeline 24 - theorem
OAI.Laughlin.Fock.four_create_bidegreeline 39