OAI/Analysis/Commutator/SchurWeylDevelopment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.SchurWeyl.tensorPower line 19
  2. lemma OAI.Kadison.SchurWeyl.tensorPower_apply line 23
  3. lemma OAI.Kadison.SchurWeyl.tensorPower_diagonal line 27
  4. lemma OAI.Kadison.SchurWeyl.tensorPower_one line 42
  5. lemma OAI.Kadison.SchurWeyl.tensorPower_mul line 47
  6. def OAI.Kadison.SchurWeyl.permutationMatrix line 55
  7. lemma OAI.Kadison.SchurWeyl.tensorPower_commute_permutation line 58
  8. def OAI.Kadison.SchurWeyl.assignmentMatrix line 82
  9. lemma OAI.Kadison.SchurWeyl.assignmentMatrix_column line 86
  10. lemma OAI.Kadison.SchurWeyl.tensorPower_assignment line 98
  11. lemma OAI.Kadison.SchurWeyl.eq_zero_of_commute_of_column_zero line 108
  12. lemma OAI.Kadison.SchurWeyl.exists_permutation_of_range line 121
  13. lemma OAI.Kadison.SchurWeyl.column_support_permutations line 136
  14. lemma OAI.Kadison.SchurWeyl.permutation_label_injective line 158
  15. theorem OAI.Kadison.SchurWeyl.commutant_tensorPower line 166
  16. lemma OAI.Kadison.SchurWeyl.complex_unit_circle_infinite line 205
  17. lemma OAI.Kadison.SchurWeyl.diagonal_unitary line 211
  18. lemma OAI.Kadison.SchurWeyl.commute_diagonal_of_unitary line 218
  19. lemma OAI.Kadison.SchurWeyl.commute_hermitian_of_unitary line 240
  20. lemma OAI.Kadison.SchurWeyl.commute_complexification line 256
  21. lemma OAI.Kadison.SchurWeyl.commute_all_of_unitary line 281
  22. theorem OAI.Kadison.SchurWeyl.commutant_unitary_tensorPower line 294