OAI/Analysis/KadisonSimilarity/FreeProduct/FreeMatrixConjugation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Matrix conjugation on the dense free-word family. Its scalar Gram matrix is unchanged, so it extends to the actual tracial Hilbert space.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.freeWordFamily line 22
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeWordFamily_total line 26
  3. def OAI.KadisonSimilarity.TracialCornerGeometry.freeConjugatedParameter line 39
  4. def OAI.KadisonSimilarity.TracialCornerGeometry.freeConjugatedFamily line 45
  5. theorem OAI.KadisonSimilarity.TracialCornerGeometry.inner_freeWord_same line 48
  6. theorem OAI.KadisonSimilarity.TracialCornerGeometry.inner_freeWord_different line 63
  7. theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_conjugated_pair line 74
  8. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeConjugatedFamily_gram line 87
  9. def OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry line 101
  10. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_family line 106
  11. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_word line 113