OAI/Analysis/Laughlin/FiniteFlux/Gram082.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Certificate.gram_8_1_1 line 9
2. theorem OAI.Laughlin.Certificate.gram_8_1_3 line 15
3. theorem OAI.Laughlin.Certificate.gram_8_1_5 line 21
4. theorem OAI.Laughlin.Certificate.gram_8_1_7 line 27
5. theorem OAI.Laughlin.Certificate.gram_8_3_3 line 33
6. theorem OAI.Laughlin.Certificate.gram_8_3_5 line 39
7. theorem OAI.Laughlin.Certificate.gram_8_3_7 line 45
8. theorem OAI.Laughlin.Certificate.gram_8_5_5 line 51
9. theorem OAI.Laughlin.Certificate.gram_8_5_7 line 57
10. theorem OAI.Laughlin.Certificate.gram_8_7_7 line 63