OAI/Analysis/KadisonKastler/SharedConjugationBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tracial conjugation comparison from the constructed common right action

  1. theorem OAI.KadisonKastler.StandardTracialPosition.right_action_eq line 17
  2. theorem OAI.KadisonKastler.norm_tracialConjugations_sub_le_of_shared_right line 35