SubalgebraCentralPairing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A dense matrix tower determines the pairing of an ambient central element against the whole subalgebra. The central element need not belong to that subalgebra.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.ambient_central_stage_pairing line 23
theorem OAI.KadisonSimilarity.TracialCornerGeometry.ambient_central_pairing_of_matrix_tower line 55
Source documentation
Central trace pairings factor against the entire matrix-generated subalgebra, by density of its trace vectors.
```
theorem ambient_central_pairing_of_matrix_tower (c : P)
    (hc : ∀ a : P, a * c = c * a) (d : D) :
    G.trace (c * (d : P)) = G.trace c * G.trace (d : P) := by
…
```