OAI/Analysis/Pureness/Cuntz/MatrixTraceCorrespondence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.TracialState.comap line 11
  2. def OAI.CuntzPureness.scalarMatrixHom line 26
  3. def OAI.CuntzPureness.singleMatrix line 35
  4. lemma OAI.CuntzPureness.singleMatrix_mul_same line 39
  5. lemma OAI.CuntzPureness.singleMatrix_mul_ne line 47
  6. lemma OAI.CuntzPureness.matrix_eq_sum_single line 57
  7. lemma OAI.CuntzPureness.trace_single_offDiagonal line 64
  8. lemma OAI.CuntzPureness.trace_single_diagonal_eq line 71
  9. lemma OAI.CuntzPureness.trace_matrix_eq_sum_diagonal line 76
  10. lemma OAI.CuntzPureness.scalarMatrix_eq_sum_single line 90
  11. lemma OAI.CuntzPureness.trace_scalarMatrix line 97
  12. theorem OAI.CuntzPureness.matrixTrace_comap_scale line 104
  13. lemma OAI.CuntzPureness.TracialState.ext line 116
  14. theorem OAI.CuntzPureness.matrixTracialState_comap line 123
  15. theorem OAI.CuntzPureness.comap_matrixTracialState line 131
  16. theorem OAI.CuntzPureness.matrix_tracialState_nonempty_iff line 142