OAI/Analysis/Laughlin/Polynomial/SymmetricTensorOrbit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Rotation.tensorPermutation line 9
2. theorem OAI.Laughlin.Rotation.tensorWeight_perm line 16
3. theorem OAI.Laughlin.Rotation.tensorWeight_eq_exists_perm line 24
4. theorem OAI.Laughlin.Rotation.tensorMatrix_perm line 39
5. theorem OAI.Laughlin.Rotation.tensorMatrix_preserves_symmetric line 44