OAI/Analysis/Laughlin/FourBody/RetainedInclusions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Spin.castSpinColumns line 9
2. theorem OAI.Laughlin.Spin.castSpinColumns_SU2 line 13
3. theorem OAI.Laughlin.Spin.castSpinColumns_isometry line 21
4. def OAI.Laughlin.Spin.fourSpinWeight line 27
5. theorem OAI.Laughlin.Spin.four_nested_weight line 29
6. theorem OAI.Laughlin.Spin.fourSpinWeight_dimension line 34
7. def OAI.Laughlin.Spin.retainedFourInclusion line 37
8. theorem OAI.Laughlin.Spin.retainedFourInclusion_column line 45
9. theorem OAI.Laughlin.Spin.retainedFourInclusion_SU2 line 53
10. theorem OAI.Laughlin.Spin.retainedFourInclusion_isometry line 61