OAI/Analysis/LaughlinFock/Sparse19.lean
16 declarations, 0 contain sorry, 0 declared as axioms
Sparse19.
- def
OAI.LaughlinFock.collectedFourData_19_0line 9 - def
OAI.LaughlinFock.collectedFourData_19_1line 36 - def
OAI.LaughlinFock.collectedFourData_19_2line 63 - def
OAI.LaughlinFock.collectedFourData_19_3line 90 - def
OAI.LaughlinFock.collectedFourData_19_4line 117 - def
OAI.LaughlinFock.collectedFourData_19_5line 144 - def
OAI.LaughlinFock.collectedFourData_19_6line 171 - def
OAI.LaughlinFock.collectedFourData_19_7line 198 - def
OAI.LaughlinFock.collectedFourData_19_8line 225 - def
OAI.LaughlinFock.collectedFourData_19_9line 252 - def
OAI.LaughlinFock.collectedFourData_19_10line 279 - def
OAI.LaughlinFock.collectedFourData_19_11line 306 - def
OAI.LaughlinFock.collectedFourData_19_12line 333 - def
OAI.LaughlinFock.collectedFourData_19_13line 360 - def
OAI.LaughlinFock.collectedFourData_19line 366 - theorem
OAI.LaughlinFock.collectedFourChecked_19line 368