OAI/Analysis/Laughlin/FiniteFlux/ComputeLDL06Batch19.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Certificate.computeLDL_19_6_0line 6 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_1line 11 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_2line 16 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_3line 21 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_4line 26 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_5line 31 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_6line 36 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_7line 41 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_8line 46 - theorem
OAI.Laughlin.Certificate.computeLDL_19_6_9line 51