OAI/Analysis/ModularTheory/OriginalRightAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

On the original coefficient algebra, the core's tracial right action is the pointwise original standard-form right action.

  1. lemma OAI.WeakPureInfiniteness.modularGauge_coefficient line 14
  2. lemma OAI.WeakPureInfiniteness.modularConjugationLp_coefficient line 26
  3. lemma OAI.WeakPureInfiniteness.modularWeightAdjointMap_coefficient line 37
  4. lemma OAI.WeakPureInfiniteness.modularTracialRightAction_coefficient line 45