OAI/Analysis/LaughlinFock/Certificate22Data.lean
71 declarations, 0 contain sorry, 0 declared as axioms
Certificate22 Data.
- def
OAI.LaughlinFock.fourYData_22line 14 - def
OAI.LaughlinFock.fourZData_22line 29 - def
OAI.LaughlinFock.fourLData_22line 44 - def
OAI.LaughlinFock.fourPivotData_22line 59 - theorem
OAI.LaughlinFock.fourOccupations_22line 62 - theorem
OAI.LaughlinFock.fourYNumber_22_1_1line 65 - theorem
OAI.LaughlinFock.fourYNumber_22_3_1line 69 - theorem
OAI.LaughlinFock.fourYNumber_22_3_3line 73 - theorem
OAI.LaughlinFock.fourYNumber_22_5_1line 77 - theorem
OAI.LaughlinFock.fourYNumber_22_5_3line 81 - theorem
OAI.LaughlinFock.fourYNumber_22_5_5line 85 - theorem
OAI.LaughlinFock.fourYNumber_22_7_1line 89 - theorem
OAI.LaughlinFock.fourYNumber_22_7_3line 93 - theorem
OAI.LaughlinFock.fourYNumber_22_7_5line 97 - theorem
OAI.LaughlinFock.fourYNumber_22_7_7line 101 - theorem
OAI.LaughlinFock.fourYNumber_22_9_1line 105 - theorem
OAI.LaughlinFock.fourYNumber_22_9_3line 109 - theorem
OAI.LaughlinFock.fourYNumber_22_9_5line 113 - theorem
OAI.LaughlinFock.fourYNumber_22_9_7line 117 - theorem
OAI.LaughlinFock.fourYNumber_22_9_9line 121 - theorem
OAI.LaughlinFock.fourYNumber_22_11_1line 125 - theorem
OAI.LaughlinFock.fourYNumber_22_11_3line 129 - theorem
OAI.LaughlinFock.fourYNumber_22_11_5line 133 - theorem
OAI.LaughlinFock.fourYNumber_22_11_7line 137 - theorem
OAI.LaughlinFock.fourYNumber_22_11_9line 141 - theorem
OAI.LaughlinFock.fourYNumber_22_11_11line 145 - theorem
OAI.LaughlinFock.fourYNumber_22_13_1line 149 - theorem
OAI.LaughlinFock.fourYNumber_22_13_3line 153 - theorem
OAI.LaughlinFock.fourYNumber_22_13_5line 157 - theorem
OAI.LaughlinFock.fourYNumber_22_13_7line 161 - theorem
OAI.LaughlinFock.fourYNumber_22_13_9line 165 - theorem
OAI.LaughlinFock.fourYNumber_22_13_11line 169 - theorem
OAI.LaughlinFock.fourYNumber_22_13_13line 173 - theorem
OAI.LaughlinFock.fourYNumber_22_15_1line 177 - theorem
OAI.LaughlinFock.fourYNumber_22_15_3line 181 - theorem
OAI.LaughlinFock.fourYNumber_22_15_5line 185 - theorem
OAI.LaughlinFock.fourYNumber_22_15_7line 189 - theorem
OAI.LaughlinFock.fourYNumber_22_15_9line 193 - theorem
OAI.LaughlinFock.fourYNumber_22_15_11line 197 - theorem
OAI.LaughlinFock.fourYNumber_22_15_13line 201 - theorem
OAI.LaughlinFock.fourYNumber_22_15_15line 205 - theorem
OAI.LaughlinFock.fourYNumber_22_17_1line 209 - theorem
OAI.LaughlinFock.fourYNumber_22_17_3line 213 - theorem
OAI.LaughlinFock.fourYNumber_22_17_5line 217 - theorem
OAI.LaughlinFock.fourYNumber_22_17_7line 221 - theorem
OAI.LaughlinFock.fourYNumber_22_17_9line 225 - theorem
OAI.LaughlinFock.fourYNumber_22_17_11line 229 - theorem
OAI.LaughlinFock.fourYNumber_22_17_13line 233 - theorem
OAI.LaughlinFock.fourYNumber_22_17_15line 237 - theorem
OAI.LaughlinFock.fourYNumber_22_17_17line 241 - theorem
OAI.LaughlinFock.fourYNumber_22_19_1line 245 - theorem
OAI.LaughlinFock.fourYNumber_22_19_3line 249 - theorem
OAI.LaughlinFock.fourYNumber_22_19_5line 253 - theorem
OAI.LaughlinFock.fourYNumber_22_19_7line 257 - theorem
OAI.LaughlinFock.fourYNumber_22_19_9line 261 - theorem
OAI.LaughlinFock.fourYNumber_22_19_11line 265 - theorem
OAI.LaughlinFock.fourYNumber_22_19_13line 269 - theorem
OAI.LaughlinFock.fourYNumber_22_19_15line 273 - theorem
OAI.LaughlinFock.fourYNumber_22_19_17line 277 - theorem
OAI.LaughlinFock.fourYNumber_22_19_19line 281 - theorem
OAI.LaughlinFock.fourYNumber_22_21_1line 285 - theorem
OAI.LaughlinFock.fourYNumber_22_21_3line 289 - theorem
OAI.LaughlinFock.fourYNumber_22_21_5line 293 - theorem
OAI.LaughlinFock.fourYNumber_22_21_7line 297 - theorem
OAI.LaughlinFock.fourYNumber_22_21_9line 301 - theorem
OAI.LaughlinFock.fourYNumber_22_21_11line 305 - theorem
OAI.LaughlinFock.fourYNumber_22_21_13line 309 - theorem
OAI.LaughlinFock.fourYNumber_22_21_15line 313 - theorem
OAI.LaughlinFock.fourYNumber_22_21_17line 317 - theorem
OAI.LaughlinFock.fourYNumber_22_21_19line 321 - theorem
OAI.LaughlinFock.fourYNumber_22_21_21line 325