OAI/Analysis/Commutator/MatrixVectorTrace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.MatrixGNS.ArraySpace line 27
  2. def OAI.Kadison.MatrixGNS.representation line 29
  3. lemma OAI.Kadison.MatrixGNS.representation_apply line 32
  4. def OAI.Kadison.MatrixGNS.algebraArray line 36
  5. lemma OAI.Kadison.MatrixGNS.algebraArray_apply line 40
  6. lemma OAI.Kadison.MatrixGNS.representation_oneArray line 43
  7. def OAI.Kadison.MatrixGNS.scale line 50
  8. lemma OAI.Kadison.MatrixGNS.scale_ne_zero line 52
  9. def OAI.Kadison.MatrixGNS.vacuum line 56
  10. lemma OAI.Kadison.MatrixGNS.representation_vacuum line 58
  11. def OAI.Kadison.MatrixGNS.trace line 62
  12. lemma OAI.Kadison.MatrixGNS.trace_vector line 71
  13. lemma OAI.Kadison.MatrixGNS.diagonal_inner line 74
  14. lemma OAI.Kadison.MatrixGNS.trace_apply line 79
  15. lemma OAI.Kadison.MatrixGNS.trace_one line 89
  16. lemma OAI.Kadison.MatrixGNS.trace_mul line 94