OAI/Analysis/Laughlin/Spin/Schur.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Rotation.spinSeparatingRoot line 9
  2. theorem OAI.Laughlin.Rotation.spinSeparatingRoot_primitive line 10
  3. theorem OAI.Laughlin.Rotation.spinSeparatingRoot_norm line 12
  4. theorem OAI.Laughlin.Rotation.torus_weight_fraction line 15
  5. theorem OAI.Laughlin.Rotation.spinSeparatingRoot_weights_injective line 26
  6. theorem OAI.Laughlin.Rotation.source_spin_commutant_scalar line 40
  7. theorem OAI.Laughlin.Rotation.source_spin_haar_schur line 72