OAI/Analysis/BoundedHochschild/FiniteGroupMultimodularity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The module identities of the contractive finite-group cochain average.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_fixed_value line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple_left line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple_right line 35
  4. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple_internal line 51
  5. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_multimodularAt line 79
  6. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_span line 128