OAI/Analysis/BoundedHochschild/BarInsertionFormula.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An explicit input formula for the bounded bar-insertion operators.

  1. def OAI.BoundedHochschild.KadisonRingrose.barPrefixTuple line 13
  2. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple_prefix_insert line 18
  3. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_prefix_value line 47