OAI/Analysis/BoundedHochschild/RightModuleAveragingExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A completely bounded map on the properly infinite algebra has a right module map in its original weak-star closed averaging orbit.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_right_module_average line 19