OAI/Analysis/KadisonKastler/RelativeIrreducibilityTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transporting a scalar relative commutant through common representations

  1. theorem OAI.KadisonKastler.relative_scalar_of_common_equivs line 18
  2. theorem OAI.KadisonKastler.relative_ambient_scalar_of_common_equivs line 46