OAI/Analysis/Laughlin/Spin/Basis2.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Laughlin.Spin.GenericCoupledIndex line 10
2. def OAI.Laughlin.Spin.genericCoupledBasis line 13
3. theorem OAI.Laughlin.Spin.genericCoupledIndex_card line 18
4. theorem OAI.Laughlin.Spin.genericCoupledBasis_isometry line 38
5. theorem OAI.Laughlin.Spin.genericCoupledBasis_complete line 60
6. theorem OAI.Laughlin.Spin.genericCoupledInclusion_isometry line 65
7. theorem OAI.Laughlin.Spin.physicalCoupledInclusion_isometry line 77