OAI/Analysis/Laughlin/FiniteFlux/ComputeGram01Batch19.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.Certificate.computeGram_19_1_1line 6 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_3line 11 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_5line 16 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_7line 21 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_9line 26 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_11line 31 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_13line 36 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_15line 41 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_17line 46 - theorem
OAI.Laughlin.Certificate.computeGram_19_1_19line 51