OAI/Analysis/LaughlinFock/Certificate10Data.lean
20 declarations, 0 contain sorry, 0 declared as axioms
Certificate10 Data.
- def
OAI.LaughlinFock.fourYData_10line 14 - def
OAI.LaughlinFock.fourZData_10line 23 - def
OAI.LaughlinFock.fourLData_10line 32 - def
OAI.LaughlinFock.fourPivotData_10line 41 - theorem
OAI.LaughlinFock.fourOccupations_10line 44 - theorem
OAI.LaughlinFock.fourYNumber_10_1_1line 47 - theorem
OAI.LaughlinFock.fourYNumber_10_3_1line 51 - theorem
OAI.LaughlinFock.fourYNumber_10_3_3line 55 - theorem
OAI.LaughlinFock.fourYNumber_10_5_1line 59 - theorem
OAI.LaughlinFock.fourYNumber_10_5_3line 63 - theorem
OAI.LaughlinFock.fourYNumber_10_5_5line 67 - theorem
OAI.LaughlinFock.fourYNumber_10_7_1line 71 - theorem
OAI.LaughlinFock.fourYNumber_10_7_3line 75 - theorem
OAI.LaughlinFock.fourYNumber_10_7_5line 79 - theorem
OAI.LaughlinFock.fourYNumber_10_7_7line 83 - theorem
OAI.LaughlinFock.fourYNumber_10_9_1line 87 - theorem
OAI.LaughlinFock.fourYNumber_10_9_3line 91 - theorem
OAI.LaughlinFock.fourYNumber_10_9_5line 95 - theorem
OAI.LaughlinFock.fourYNumber_10_9_7line 99 - theorem
OAI.LaughlinFock.fourYNumber_10_9_9line 103