OAI/Analysis/LaughlinFock/Sparse1703.lean
12 declarations, 0 contain sorry, 0 declared as axioms
Sparse1703.
- def
OAI.LaughlinFock.collectedFourData_17_46line 9 - def
OAI.LaughlinFock.collectedFourData_17_47line 36 - def
OAI.LaughlinFock.collectedFourData_17_48line 63 - def
OAI.LaughlinFock.collectedFourData_17_49line 90 - def
OAI.LaughlinFock.collectedFourData_17_50line 117 - def
OAI.LaughlinFock.collectedFourData_17_51line 144 - def
OAI.LaughlinFock.collectedFourData_17_52line 171 - def
OAI.LaughlinFock.collectedFourData_17_53line 198 - def
OAI.LaughlinFock.collectedFourData_17_54line 225 - def
OAI.LaughlinFock.collectedFourData_17_55line 252 - def
OAI.LaughlinFock.collectedFourData_17line 279 - theorem
OAI.LaughlinFock.collectedFourChecked_17line 281