OAI/Analysis/Laughlin/Operators/GlobalPairCube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.pairAffineChart_coefficient line 10
2. theorem OAI.Laughlin.affine_pair_cubes_of_bracket_dvd line 28
3. theorem OAI.Laughlin.affine_pair_cubes_iff_bracket_dvd line 53
4. theorem OAI.Laughlin.energy_eq_zero_iff_global_pair_cubes line 61