KaplanskyColumns.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Matrix-column Kaplansky approximation in the original C-star algebra.

theorem OAI.KadisonSimilarity.kaplanskyColumnApproximation line 16
Source documentation
The column approximation input follows from the proved unit-ball Kaplansky theorem. The constructed column even has norm at most one.
```
theorem kaplanskyColumnApproximation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    KaplanskyColumnApproximation σ := by
…
```
Mentions: OAI.KadisonSimilarity.KaplanskyColumnApproximation