OAI/Analysis/Laughlin/FiniteFlux/ComputeRow0519Batch20.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_0line 7 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_1line 11 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_2line 15 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_3line 19 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_4line 23 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_5line 27 - theorem
OAI.Laughlin.Certificate.computeRow_20_5_19_6line 31