OAI/Analysis/KadisonKastler/PureRestrictionFactorization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Product values from a pure restriction

An ambient state whose restriction to one algebra is pure factors against every element commuting with that algebra.

  1. theorem OAI.KadisonKastler.pure_restriction_commuting_factorization line 19