SpatialProductState.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Product vector states and centralization on the second tensor leg

Finite spatial matrix images give the product-state identity on a dense star algebra. The actual strong-density theorem extends centralization to the spatial von Neumann product.

theorem OAI.KadisonKastler.productVectorState_spatialTensor line 26
theorem OAI.KadisonKastler.spatialRight_centralizes_simple_tensor line 33
theorem OAI.KadisonKastler.spatialRight_productStateCentralizes line 46
Source documentation
The second-leg state centralizer remains in the centralizer of a product vector state, for the actual spatial von Neumann product.
```
theorem spatialRight_productStateCentralizes
    (hK : PublishedKaplanskyDensity.{u}) (M : VonNeumannAlgebra H)
    (P : ProductMatrixStages (H := K)) (Ω : H) (u : K →L[ℂ] K)
…
```
Mentions: OAI.KadisonKastler.ProductMatrixStages