OAI/Analysis/BoundedHochschild/FactorPrimitive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded Hochschild primitives on diffuse finite factors, with and without separable predual.

  1. theorem OAI.BoundedHochschild.primitive_of_separable_normal_factor line 23
  2. theorem OAI.BoundedHochschild.primitive_of_separable_factor line 38
  3. theorem OAI.BoundedHochschild.primitive_of_normal_factor line 68
  4. theorem OAI.BoundedHochschild.primitive_of_factor line 120