OAI/Analysis/KadisonSimilarity/FreeProduct/FreeMatrixFactorAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The free-word isometry fixes the base algebra and intertwines left multiplication by the matrix factor.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_base line 23
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_one line 30
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_other_word line 33
  4. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_other line 47