OAI/Analysis/Pureness/Stabilization/MatrixTrace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzTrace.Positive.exists_starMul_factor line 13
  2. lemma OAI.CuntzTrace.Positive.matrix_diagonal_nonneg line 17
  3. def OAI.CuntzTrace.Positive.matrixDiagonal line 24
  4. lemma OAI.CuntzTrace.Positive.matrixDiagonal_continuous line 27
  5. lemma OAI.CuntzTrace.Positive.matrixDiagonal_zero line 34
  6. lemma OAI.CuntzTrace.Positive.matrixDiagonal_add line 38
  7. lemma OAI.CuntzTrace.Positive.matrixDiagonal_smul line 42
  8. lemma OAI.CuntzTrace.Positive.matrixDiagonal_starMul line 45
  9. lemma OAI.CuntzTrace.Positive.matrixDiagonal_mulStar line 50
  10. def OAI.CuntzTrace.ExtendedTrace.matrixTrace line 58
  11. theorem OAI.CuntzTrace.ExtendedTrace.matrixTrace_apply line 71
  12. def OAI.CuntzTrace.matrixCorner line 77
  13. lemma OAI.CuntzTrace.Positive.matrixDiagonal_corner line 98
  14. theorem OAI.CuntzTrace.ExtendedTrace.matrixTrace_corner line 110
  15. lemma OAI.CuntzTrace.ExtendedTrace.matrixTrace_pullback_corner line 116
  16. theorem OAI.CuntzTrace.ExtendedTrace.matrixRank_corner line 121