OAI/Analysis/BoundedHochschild/MultimodularMergeBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Module balance survives an adjacent-input multiplication, on either side of the balanced pair.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.merge_balance_before_left line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.merge_balance_before_right line 26
  3. lemma OAI.BoundedHochschild.KadisonRingrose.merge_balance_after_left line 40
  4. lemma OAI.BoundedHochschild.KadisonRingrose.merge_balance_after_right line 54