OAI/Analysis/KadisonKastler/ExpectedFromOneBicentralizer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The expected matrix subfactor needs one scalar bicentralizer

Faithful-state homogeneity transports scalarity to the other states used in the finite-matrix refinement. The chosen reference state is arbitrary.

  1. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_one_bicentralizer line 24