OAI/Analysis/KadisonKastler/RegularCoreConjugateGenerators.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugation of the regular generators

The regular modular conjugation sends the represented algebra to the constant right algebra. Its formula is proved on actual L2 classes.

  1. theorem OAI.KadisonKastler.unitary_star_apply_apply line 24
  2. theorem OAI.KadisonKastler.regularCoreConjugation_embedding line 29
  3. theorem OAI.KadisonKastler.regularCoreConjugation_translation line 58