OAI/Analysis/Laughlin/Spin/Basis.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Laughlin.Spin.CoupledIndex line 8
2. theorem OAI.Laughlin.Spin.fin_sum_values line 10
3. theorem OAI.Laughlin.Spin.coupledIndex_card line 19
4. def OAI.Laughlin.Spin.coupledBasisMatrix line 36
5. theorem OAI.Laughlin.Spin.coupledBasis_isometry line 40
6. theorem OAI.Laughlin.Spin.coupledBasis_complete line 65
7. theorem OAI.Laughlin.Spin.coupledBasis_eigen line 70
8. theorem OAI.Laughlin.Spin.threeGram_diagonalization line 78