OAI/Analysis/KadisonKastler/KMSUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of a KMS implementation for a faithful cyclic vector

State-preserving symmetries commute with the constructed modular group. The Gaussian strip argument then identifies their actions, and cyclicity identifies the implementations themselves.

  1. theorem OAI.KadisonKastler.kmsGroup_eq_constructed line 22