OAI/Analysis/Laughlin/Polynomial/SymmetricTensorRange.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Rotation.tensorWeight_le line 8
  2. theorem OAI.Laughlin.Rotation.tensorWeight_surjective line 12
  3. def OAI.Laughlin.Rotation.tensorWeightRepresentative line 20
  4. theorem OAI.Laughlin.Rotation.tensorWeightRepresentative_weight line 22
  5. def OAI.Laughlin.Rotation.symmetricTensorInclusion line 25
  6. theorem OAI.Laughlin.Rotation.symmetricTensorInclusion_isometry line 28
  7. theorem OAI.Laughlin.Rotation.symmetricTensorInclusion_mulVec line 35
  8. theorem OAI.Laughlin.Rotation.symmetricTensor_range line 49
  9. theorem OAI.Laughlin.Rotation.symmetricTensor_projector_fixed line 66