OAI/Analysis/Commutator/InvariantForms.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.SchurWeyl.tensorMatrices line 20
  2. lemma OAI.Kadison.SchurWeyl.tensorMatrices_mul line 24
  3. lemma OAI.Kadison.SchurWeyl.tensorMatrices_single line 33
  4. def OAI.Kadison.SchurWeyl.traceForm line 47
  5. lemma OAI.Kadison.SchurWeyl.traceForm_apply line 53
  6. lemma OAI.Kadison.SchurWeyl.traceForm_single line 59
  7. def OAI.Kadison.SchurWeyl.coefficientMatrix line 64
  8. lemma OAI.Kadison.SchurWeyl.traceForm_coefficientMatrix line 68
  9. lemma OAI.Kadison.SchurWeyl.coefficientMatrix_traceForm line 77
  10. lemma OAI.Kadison.SchurWeyl.traceForm_injective line 82
  11. lemma OAI.Kadison.SchurWeyl.traceForm_conjugate line 87
  12. lemma OAI.Kadison.SchurWeyl.coefficientMatrix_commute_unitary line 97
  13. theorem OAI.Kadison.SchurWeyl.invariant_multilinear_form line 116