OAI/Analysis/Laughlin/ThreeBody/TraceReadout.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Spin.phasedThreeDescendant line 8
2. theorem OAI.Laughlin.Spin.phasedThreeDescendant_off line 12
3. theorem OAI.Laughlin.Spin.phasedThreeDescendant_at_level line 19
4. theorem OAI.Laughlin.Spin.threeBodyLevelVector_dot line 28
5. theorem OAI.Laughlin.Spin.phasedThreeDescendant_unit_off line 42
6. theorem OAI.Laughlin.Spin.threeBodyLevelVector_descendant_off line 52
7. theorem OAI.Laughlin.Spin.threeBodyLevelVector_descendant line 66