OAI/Analysis/Laughlin/FourBody/Copies.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Spin.tensorPairInclusion line 9
2. theorem OAI.Laughlin.Spin.tensorPairInclusion_isometry line 13
3. theorem OAI.Laughlin.Spin.isometry_vectorNormSq line 24
4. def OAI.Laughlin.Spin.fourBodyCopy line 37
5. theorem OAI.Laughlin.Spin.phased_generic_norm line 44
6. theorem OAI.Laughlin.Spin.fourBodyCopy_norm line 53
7. theorem OAI.Laughlin.Spin.fourBodyCopy_coordinate line 60