OAI/Analysis/FreeWords/TensorUnitaryEnd.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKWeingarten.prod_delta_eq line 15
  2. theorem OAI.KKWeingarten.lieMatrix_single_apply line 31
  3. theorem OAI.KKWeingarten.lieMatrix_single_mul line 56
  4. theorem OAI.KKWeingarten.mul_lieMatrix_single line 69
  5. theorem OAI.KKWeingarten.lieInvariant_of_tensor_commute line 87
  6. theorem OAI.KKWeingarten.tensor_permMatrix line 95
  7. theorem OAI.KKWeingarten.labelInvariant_of_tensor_commute line 108
  8. theorem OAI.KKWeingarten.unitary_tensor_commutant line 128