OAI/Analysis/BoundedHochschild/NormalBarOperators.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separate normality is retained by finite prefix averaging and by each bounded bar-insertion operator.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.separatelyNormal_curryMid line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_normal line 29
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_normal line 38
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarInsertion_normal line 47
  5. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_normal line 57