OAI/Analysis/BoundedHochschild/CommutativePrimitives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded primitives for commutative dual algebras.

  1. lemma OAI.BoundedHochschild.exists_finite_commuting_invariant line 24
  2. theorem OAI.BoundedHochschild.exists_commuting_invariant line 45
  3. lemma OAI.BoundedHochschild.right_module_of_all_translates line 78
  4. theorem OAI.BoundedHochschild.primitive_of_commutative line 99
  5. theorem OAI.BoundedHochschild.primitive_of_commutative_wstar line 111