OAI/Analysis/KadisonKastler/PolarCommutantEquality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The polar commutant equality from the averaged inclusion

  1. theorem OAI.KadisonKastler.tomitaPolarConjugation_commutant_eq_of_inclusion line 16