SubalgebraMatrixColumns.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Regrouping a countable matrix system inside a specified von Neumann subalgebra. Only the matrix transitions, not the original ambient columns, are required to belong to that subalgebra.

theorem OAI.BoundedHochschild.KadisonRingrose.finite_columns_in_subalgebra line 22