OAI/Analysis/KadisonKastler/SpatialStateScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

State-scaling identities under spatial inclusions and conjugations

  1. theorem OAI.KadisonKastler.productVectorState_tensor_slice line 22
  2. theorem OAI.KadisonKastler.StateScales.spatialLeft line 26
  3. theorem OAI.KadisonKastler.productVectorState_spatial_conjugate line 33
  4. theorem OAI.KadisonKastler.StateScales.spatial_conjugate line 38