OAI/Analysis/KadisonKastler/RegularPointwiseConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise antiunitaries on the regular Hilbert space

These concrete maps will provide the conjugation for the modular core.

  1. def OAI.KadisonKastler.regularPointwiseConjugation line 18
  2. theorem OAI.KadisonKastler.regularPointwiseConjugation_apply_ae line 50
  3. theorem OAI.KadisonKastler.regularPointwiseConjugation_involutive line 56