OAI/Analysis/BoundedHochschild/CountableMatrixTypeI.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The generated countable matrix algebra is type I: its abelian diagonal has full central support, since all diagonal projections are equivalent and their sum is the ambient unit.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_typeI line 20