OAI/Analysis/KadisonSimilarity/Tracial/TracialAdjointBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The same corner hypotheses hold for the adjoint operator, so the propagation argument supplies both errors in the final compression.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.adjoint_commutes_with_base line 17
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.adjoint_corner_commutator_bound line 25