OAI/Analysis/Commutator/MatrixColumnCorner.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.MatrixColumnCorner.minimal_projection line 20
  2. lemma OAI.Kadison.MatrixColumnCorner.full_column line 24
  3. lemma OAI.Kadison.MatrixColumnCorner.trace_minimal line 43
  4. lemma OAI.Kadison.MatrixColumnCorner.exists_small_stage line 51
  5. lemma OAI.Kadison.projection_symmetry_square line 69
  6. lemma OAI.Kadison.projection_symmetry_selfadjoint line 73
  7. def OAI.Kadison.projectionSymmetry line 76
  8. lemma OAI.Kadison.projectionSymmetry_coe line 79
  9. lemma OAI.Kadison.projectionSymmetry_half line 81
  10. lemma OAI.Kadison.projectionSymmetry_left line 85
  11. lemma OAI.Kadison.projectionSymmetry_right line 89
  12. lemma OAI.Kadison.unitary_dihedral line 94
  13. lemma OAI.Kadison.isStarProjection_corner line 103