OAI/Analysis/LaughlinFock/Sparse1027.lean
14 declarations, 0 contain sorry, 0 declared as axioms
Sparse1027.
- def
OAI.LaughlinFock.collectedFourData_10_7_34line 10 - def
OAI.LaughlinFock.collectedFourData_10_7_35line 57 - def
OAI.LaughlinFock.collectedFourData_10_7_36line 81 - def
OAI.LaughlinFock.collectedFourData_10_7_37line 112 - def
OAI.LaughlinFock.collectedFourData_10_7_38line 151 - def
OAI.LaughlinFock.collectedFourData_10_7_39line 198 - def
OAI.LaughlinFock.collectedFourData_10_7_40line 245 - def
OAI.LaughlinFock.collectedFourData_10_7_41line 292 - def
OAI.LaughlinFock.collectedFourData_10_7_42line 339 - def
OAI.LaughlinFock.collectedFourData_10_7_43line 386 - def
OAI.LaughlinFock.collectedFourData_10_7line 433 - theorem
OAI.LaughlinFock.collectedFourChecked_10_7line 480 - def
OAI.LaughlinFock.collectedFourData_10line 483 - theorem
OAI.LaughlinFock.collectedFourChecked_10line 486