OAI/Analysis/KadisonSimilarity/FreeProduct/FreeMatrixConjugationUnitary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Inverse matrix conjugations on the actual free word Hilbert space.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_inverse line 22
  2. def OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationUnitary line 50