OAI/Analysis/KadisonKastler/ModularCoisometryBicentralizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar bicentralizers from the constructed modular coisometries

Only the fixed reference state is used. No state homogeneity, absorption classification, or scalar-bicentralizer premise enters this implication.

  1. theorem OAI.KadisonKastler.vector_bicentralizer_scalar_of_modular_coisometries line 24
  2. theorem OAI.KadisonKastler.state_bicentralizer_scalar_of_modular_coisometries line 40