OAI/Analysis/Laughlin/Spin/Mixing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Rotation.tensorWeight_sum_const line 8
  2. theorem OAI.Laughlin.Rotation.symmetricTensorInclusion_column_sum line 18
  3. theorem OAI.Laughlin.Rotation.tensorMatrix_uniform_first_column line 32
  4. def OAI.Laughlin.Rotation.sourceMixer line 48
  5. theorem OAI.Laughlin.Rotation.sourceSpinRepresentation_mixer_column line 65
  6. theorem OAI.Laughlin.Rotation.sourceSpinRepresentation_mixer_column_ne_zero line 78