OAI/Analysis/BoundedHochschild/MultimodularGenerators.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

It suffices to verify the module identities on matrix units: their linearity gives the algebraic identities, and normality gives the weak-star identities used in the primitive construction.

  1. structure OAI.BoundedHochschild.KadisonRingrose.MultimodularAt line 16
  2. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_one line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.linear_maps_eq_on_span line 26
  4. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_of_span line 37
  5. theorem OAI.BoundedHochschild.KadisonRingrose.multimodular_of_matrixUnits line 66
  6. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_normal_matrix_units line 91