OAI/Analysis/KadisonKastler/NonunitalFiberCenter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar centers of nonunital representation ranges

These adapters keep the range Hilbert space and its unit projection inside one definition when a common source is restricted to a smaller algebra.

  1. def OAI.KadisonKastler.NonunitalFiberScalarCenter line 22
  2. theorem OAI.KadisonKastler.nonunitalFiberScalarCenter_restrict_starLift line 26
  3. theorem OAI.KadisonKastler.nonunitalFiberScalarCenter_restrict_comp line 33
  4. theorem OAI.KadisonKastler.fixedFiber_scalarCenter_of_nonunital line 42