OAI/Analysis/KadisonKastler/PairedMatrixColumn.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The partial isometry from a matrix corner to central vectors

This is the algebraic corner map in Haagerup, Acta Math.158(1987), Lemma3.5. Its initial projection is the matching minimal corner; its final projection is the finite-matrix central-vector projection.

  1. theorem OAI.KadisonKastler.matchingEntry_mul line 26
  2. theorem OAI.KadisonKastler.matchingEntry_star line 37
  3. def OAI.KadisonKastler.pairedMatrixColumn line 41
  4. theorem OAI.KadisonKastler.pairedMatrixColumn_scalar_sq line 46
  5. theorem OAI.KadisonKastler.pairedMatrixColumn_star line 56
  6. theorem OAI.KadisonKastler.pairedMatrixColumn_initial line 69
  7. theorem OAI.KadisonKastler.pairedMatrixColumn_final line 82