UnconditionalSimilarity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The universal commutator estimate and finite cyclic reduction imply similarity for every bounded unital representation.

theorem OAI.KadisonSimilarity.similarityTheorem line 16
Source documentation
Theorem thm:similarity: every bounded unital complex-algebra representation of a unital C-star algebra is similar to a star representation.
Distinct definitions of this name: ComparatorChallenges/KadisonSimilarity.lean:115 (same statement text; different proof or body). Qualify references as OAI.KadisonSimilarity.similarityTheorem@path.
```
theorem similarityTheorem : SimilarityTheorem.{u,v} := by
…
```
theorem OAI.KadisonSimilarity.kirchbergDerivationCriterion_proved line 24
Source documentation
The universal estimate implies the derivation criterion for every algebra.
```
theorem kirchbergDerivationCriterion_proved (A : Type u) [CStarAlgebra A] :
    KirchbergDerivationCriterion.{u,v} A := by
…
```