OAI/Analysis/BoundedHochschild/TypeIMatrixColumns.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous matrix systems from equivalent orthogonal abelian projections.

  1. def OAI.BoundedHochschild.KadisonRingrose.matrixSystemOfColumns line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSystemOfColumns_diagonal line 44
  3. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSystemOfColumns_abelian line 53