OAI/Analysis/Commutator/FreeSymmetry16.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.TracialGNS.sumConjugationIso line 42
  2. lemma OAI.Kadison.TracialGNS.sumConjugationIso_pair line 45
  3. lemma OAI.Kadison.TracialGNS.sumConjugationIso_toCLM line 51
  4. def OAI.Kadison.TracialGNS.freeConjugation line 64
  5. lemma OAI.Kadison.TracialGNS.freeConjugation_comp line 67
  6. lemma OAI.Kadison.TracialGNS.conjugation_one line 73
  7. lemma OAI.Kadison.TracialGNS.conjugation_mul line 82
  8. lemma OAI.Kadison.TracialGNS.wordConjugation_one line 93
  9. lemma OAI.Kadison.TracialGNS.wordConjugation_mul line 101
  10. lemma OAI.Kadison.TracialGNS.sumConjugationIso_one line 111
  11. lemma OAI.Kadison.TracialGNS.sumConjugationIso_mul line 118
  12. lemma OAI.Kadison.TracialGNS.freeConjugation_one line 129
  13. lemma OAI.Kadison.TracialGNS.freeConjugation_mul line 136
  14. lemma OAI.Kadison.TracialGNS.freeConjugation_star_left line 145
  15. lemma OAI.Kadison.TracialGNS.freeConjugation_surjective line 149