OAI/Analysis/Commutator/MatrixDiagonal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.MatrixDiagonal.diagonal line 21
  2. lemma OAI.Kadison.MatrixDiagonal.diagonal_apply line 24
  3. lemma OAI.Kadison.MatrixDiagonal.single_left line 28
  4. lemma OAI.Kadison.MatrixDiagonal.single_right line 37
  5. lemma OAI.Kadison.MatrixDiagonal.commutes line 46
  6. lemma OAI.Kadison.MatrixDiagonal.cut line 58
  7. lemma OAI.Kadison.MatrixDiagonal.star_diagonal line 63
  8. lemma OAI.Kadison.MatrixDiagonal.mul_diagonal line 67
  9. lemma OAI.Kadison.MatrixDiagonal.projection line 78
  10. lemma OAI.Kadison.MatrixDiagonal.at_unit line 86
  11. lemma OAI.Kadison.MatrixDiagonal.fixed line 90
  12. lemma OAI.Kadison.MatrixDiagonal.matrix_block line 103
  13. lemma OAI.Kadison.MatrixDiagonal.central_of_commutes_diagonal line 111