OAI/Analysis/KadisonKastler/CoisometryStateHomogeneity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Faithful state homogeneity from the constructed modular coisometries

This is the state homogeneity needed by the two-ratio product application; no homogeneity theorem for arbitrary type III₁ factors is assumed.

  1. theorem OAI.KadisonKastler.stateHomogeneity_of_modular_coisometries line 23