OAI/Analysis/Laughlin/FourBody/TensorIntertwining.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Laughlin.Spin.FourTensorIndex line 11
2. def OAI.Laughlin.Spin.fourTensorInclusion line 13
3. def OAI.Laughlin.Spin.fourTensorRepresentation line 21
4. theorem OAI.Laughlin.Spin.fourTensorRepresentation_continuous line 28
5. theorem OAI.Laughlin.Spin.fourTensorRepresentation_inv line 34
6. theorem OAI.Laughlin.Spin.fourTensorInclusion_SU2 line 39
7. def OAI.Laughlin.Spin.fourWedgeInclusion line 58
8. theorem OAI.Laughlin.Spin.fourTensorInclusion_coordinate line 64
9. theorem OAI.Laughlin.Spin.fourWedgeInclusion_tensor_coordinate line 82