OAI/Analysis/BoundedHochschild/NormalFactorCandidates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compact factorization construction for the given W*-algebra predual.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.normalGNS_representation_ball_closed line 16
  2. theorem OAI.BoundedHochschild.KadisonRingrose.normalGNS_factorization line 20