KaplanskyDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Discharging the finite-test Kaplansky density input

The self-adjoint contraction case was proved by the rational bounded transform. The two-by-two self-adjoint matrix trick gives the general case without a loss in the contraction bound.

theorem OAI.KadisonKastler.norm_entry_le line 29
theorem OAI.KadisonKastler.publishedKaplanskyDensity line 40
Source documentation
Kaplansky density in precisely the finite-test formulation used by the conditional main theorem. This proof has no published hypotheses.
```
theorem publishedKaplanskyDensity : PublishedKaplanskyDensity.{u} := by
…
```