OAI/Analysis/KadisonSimilarity/FreeProduct/FreeMatrixBaseAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Centering the first two letters proves covariance for the base factor.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrix_base_product line 23
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.freeMatrixConjugationIsometry_base_left line 91