OAI/Analysis/Laughlin/Spin/PairDecomposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.pairSpinorPolynomial_orbitals line 11
2. theorem OAI.Laughlin.spinPolynomial_pair_decomposition line 23
3. theorem OAI.Laughlin.bracket_cube_dvd_spinPolynomial_of_slices line 42
4. theorem OAI.Laughlin.energy_zero_global_pair_cubes line 52
5. theorem OAI.Laughlin.zero_energy_state_eq_laughlin line 59