OAI/Analysis/LaughlinFock/Sparse1003.lean
21 declarations, 0 contain sorry, 0 declared as axioms
Sparse1003.
- def
OAI.LaughlinFock.collectedFourData_10_0_40line 10 - def
OAI.LaughlinFock.collectedFourData_10_0_41line 51 - def
OAI.LaughlinFock.collectedFourData_10_0_42line 95 - def
OAI.LaughlinFock.collectedFourData_10_0_43line 136 - def
OAI.LaughlinFock.collectedFourData_10_0line 180 - theorem
OAI.LaughlinFock.collectedFourChecked_10_0line 227 - def
OAI.LaughlinFock.collectedFourData_10_1_0line 230 - def
OAI.LaughlinFock.collectedFourData_10_1_1line 234 - def
OAI.LaughlinFock.collectedFourData_10_1_2line 244 - def
OAI.LaughlinFock.collectedFourData_10_1_3line 262 - def
OAI.LaughlinFock.collectedFourData_10_1_4line 288 - def
OAI.LaughlinFock.collectedFourData_10_1_5line 321 - def
OAI.LaughlinFock.collectedFourData_10_1_6line 360 - def
OAI.LaughlinFock.collectedFourData_10_1_7line 404 - def
OAI.LaughlinFock.collectedFourData_10_1_8line 452 - def
OAI.LaughlinFock.collectedFourData_10_1_9line 456 - def
OAI.LaughlinFock.collectedFourData_10_1_10line 466 - def
OAI.LaughlinFock.collectedFourData_10_1_11line 484 - def
OAI.LaughlinFock.collectedFourData_10_1_12line 510 - def
OAI.LaughlinFock.collectedFourData_10_1_13line 543 - def
OAI.LaughlinFock.collectedFourData_10_1_14line 582