OAI/Analysis/KadisonKastler/MatrixCentralProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit finite-matrix central-vector projection

Haagerup, Acta Math. 158 (1987), Lemma 3.5: the central-vector projection is the normalized sum of matching left and conjugate-right matrix units. The formula is proved from the matrix-unit relations and commutation.

  1. def OAI.KadisonKastler.matrixCentralProjection line 23
  2. theorem OAI.KadisonKastler.matrixCentralProjection_eq line 28