OAI/Analysis/Commutator/TracialConjugation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.TracialGNS.rightMul_mem_unitary line 16
  2. def OAI.Kadison.TracialGNS.conjugation line 25
  3. lemma OAI.Kadison.TracialGNS.conjugation_coe line 34
  4. lemma OAI.Kadison.TracialGNS.conjugation_vacuum line 41
  5. def OAI.Kadison.TracialGNS.algebraVector line 45
  6. lemma OAI.Kadison.TracialGNS.algebraVector_apply line 48
  7. lemma OAI.Kadison.TracialGNS.inner_algebraVector line 50
  8. lemma OAI.Kadison.TracialGNS.inner_vacuum_algebraVector line 55
  9. lemma OAI.Kadison.TracialGNS.algebraVector_dense line 60