OAI/Analysis/KadisonKastler/ModularCentralizerFixed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From fixed centralizer vectors to fixed operators

Normalization and separation of the state vector upgrade the fixed-vector identity to a fixed-operator identity.

  1. theorem OAI.KadisonKastler.modularStrongGroup_centralizer_fixed line 19