OAI/Analysis/BoundedHochschild/MultimodularMerges.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Multiplying adjacent inputs is compatible with module balance. These identities supply the interior faces of the relative Hochschild complex.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.mergeInputs_left_module line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.mergeInputs_right_module line 31
  3. lemma OAI.BoundedHochschild.KadisonRingrose.mergeInputs_balance_at line 52