OAI/Analysis/LaughlinFock/Certificate09Data.lean
20 declarations, 0 contain sorry, 0 declared as axioms
Certificate09 Data.
- def
OAI.LaughlinFock.fourYData_9line 14 - def
OAI.LaughlinFock.fourZData_9line 23 - def
OAI.LaughlinFock.fourLData_9line 32 - def
OAI.LaughlinFock.fourPivotData_9line 41 - theorem
OAI.LaughlinFock.fourOccupations_9line 44 - theorem
OAI.LaughlinFock.fourYNumber_9_1_1line 47 - theorem
OAI.LaughlinFock.fourYNumber_9_3_1line 51 - theorem
OAI.LaughlinFock.fourYNumber_9_3_3line 55 - theorem
OAI.LaughlinFock.fourYNumber_9_5_1line 59 - theorem
OAI.LaughlinFock.fourYNumber_9_5_3line 63 - theorem
OAI.LaughlinFock.fourYNumber_9_5_5line 67 - theorem
OAI.LaughlinFock.fourYNumber_9_7_1line 71 - theorem
OAI.LaughlinFock.fourYNumber_9_7_3line 75 - theorem
OAI.LaughlinFock.fourYNumber_9_7_5line 79 - theorem
OAI.LaughlinFock.fourYNumber_9_7_7line 83 - theorem
OAI.LaughlinFock.fourYNumber_9_9_1line 87 - theorem
OAI.LaughlinFock.fourYNumber_9_9_3line 91 - theorem
OAI.LaughlinFock.fourYNumber_9_9_5line 95 - theorem
OAI.LaughlinFock.fourYNumber_9_9_7line 99 - theorem
OAI.LaughlinFock.fourYNumber_9_9_9line 103