OAI/Analysis/LaughlinFock/Certificate08Data.lean
15 declarations, 0 contain sorry, 0 declared as axioms
Certificate08 Data.
- def
OAI.LaughlinFock.fourYData_8line 14 - def
OAI.LaughlinFock.fourZData_8line 22 - def
OAI.LaughlinFock.fourLData_8line 30 - def
OAI.LaughlinFock.fourPivotData_8line 38 - theorem
OAI.LaughlinFock.fourOccupations_8line 41 - theorem
OAI.LaughlinFock.fourYNumber_8_1_1line 44 - theorem
OAI.LaughlinFock.fourYNumber_8_3_1line 48 - theorem
OAI.LaughlinFock.fourYNumber_8_3_3line 52 - theorem
OAI.LaughlinFock.fourYNumber_8_5_1line 56 - theorem
OAI.LaughlinFock.fourYNumber_8_5_3line 60 - theorem
OAI.LaughlinFock.fourYNumber_8_5_5line 64 - theorem
OAI.LaughlinFock.fourYNumber_8_7_1line 68 - theorem
OAI.LaughlinFock.fourYNumber_8_7_3line 72 - theorem
OAI.LaughlinFock.fourYNumber_8_7_5line 76 - theorem
OAI.LaughlinFock.fourYNumber_8_7_7line 80