OAI/Analysis/ModularTheory/CoreDualAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The dual action as actual star algebra automorphisms of the concrete modular core, including its group law.

  1. lemma OAI.WeakPureInfiniteness.modularDualConjugation_apply line 18
  2. lemma OAI.WeakPureInfiniteness.modularDualConjugation_comp line 23
  3. lemma OAI.WeakPureInfiniteness.modularDualConjugation_zero line 33
  4. def OAI.WeakPureInfiniteness.modularCoreDualHom line 39
  5. lemma OAI.WeakPureInfiniteness.modularCoreDualHom_comp line 46
  6. lemma OAI.WeakPureInfiniteness.modularCoreDualHom_zero line 53
  7. def OAI.WeakPureInfiniteness.modularCoreDualAction line 59
  8. lemma OAI.WeakPureInfiniteness.modularCoreDualAction_comp line 70