OAI/Analysis/Laughlin/FourBody/Matrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Certificate.copyWeight line 9
2. def OAI.Laughlin.Certificate.middleRational line 12
3. def OAI.Laughlin.Certificate.compressedRational line 17
4. theorem OAI.Laughlin.Certificate.compressed_positive_of_gram_zero line 20
5. theorem OAI.Laughlin.Certificate.gram_one_zero line 28
6. theorem OAI.Laughlin.Certificate.gram_two_zero line 29
7. theorem OAI.Laughlin.Certificate.gram_three_zero line 30
8. theorem OAI.Laughlin.Certificate.gram_four_zero line 31
9. theorem OAI.Laughlin.Certificate.gram_six_zero line 32
10. theorem OAI.Laughlin.Certificate.zero_blocks_positive line 34