OAI/Analysis/Laughlin/Spin/CopySchur.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Rotation.copyMatrix line 10
  2. theorem OAI.Laughlin.Rotation.copyMatrix_mul line 14
  3. theorem OAI.Laughlin.Rotation.copyMatrix_one line 21
  4. def OAI.Laughlin.Rotation.copiedSpinRepresentation line 30
  5. theorem OAI.Laughlin.Rotation.copied_conjugateOrbit_block line 36
  6. theorem OAI.Laughlin.Rotation.source_spin_copy_haar_schur line 46
  7. theorem OAI.Laughlin.Rotation.source_highest_copy_orbit_resolution line 54