OAI/Analysis/Laughlin/FourBody/Support.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Spin.realOuter_mulVec_row line 9
2. theorem OAI.Laughlin.Spin.fourBodyTermMatrix_high_copy line 16
3. theorem OAI.Laughlin.Spin.list_sum_mul_zero line 28
4. theorem OAI.Laughlin.Spin.physicalFourBodyMatrix_high_copy line 35
5. theorem OAI.Laughlin.Spin.real_matrix_mul_zero_complex line 52
6. theorem OAI.Laughlin.Spin.physicalFourBodyMatrix_high_wedge_copy line 60
7. theorem OAI.Laughlin.Spin.physicalFourBodyHaar_high_copy line 65