OAI/Analysis/BoundedHochschild/AlgebraicMatrixPrimitives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The properly infinite primitive endpoint needs module identities only on the algebraic countable matrix units. Separate normality is supplied by the proved normal reduction, retaining those identities.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_algebraic_matrix_multimodular line 19
  2. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_matrix_units line 35