OAI/Analysis/Commutator/TracialRightClosure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.TracialGNS.operatorConjugate_mul line 22
  2. lemma OAI.Kadison.TracialGNS.operatorConjugate_norm_le line 27
  3. lemma OAI.Kadison.TracialGNS.operatorConjugate_norm line 34
  4. lemma OAI.Kadison.TracialGNS.operatorConjugate_left line 41
  5. lemma OAI.Kadison.TracialGNS.operatorConjugate_right line 57
  6. lemma OAI.Kadison.TracialGNS.bicommutant_star line 62
  7. lemma OAI.Kadison.TracialGNS.operatorConjugate_bicommutant_mem_commutant line 69
  8. def OAI.Kadison.TracialGNS.rightOperator line 77
  9. lemma OAI.Kadison.TracialGNS.rightOperator_original line 80
  10. lemma OAI.Kadison.TracialGNS.rightOperator_norm line 84
  11. lemma OAI.Kadison.TracialGNS.rightOperator_mul line 88
  12. theorem OAI.Kadison.TracialGNS.commutation line 93
  13. lemma OAI.Kadison.TracialGNS.starMap_bicommutant_vacuum line 105
  14. lemma OAI.Kadison.TracialGNS.bicommutant_vacuum_separating line 127
  15. lemma OAI.Kadison.TracialGNS.bicommutant_trace line 139