OAI/Analysis/BoundedHochschild/CountableMatrixSpan.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The algebraic countable matrix algebra consists of finite linear combinations of its matrix units and the ambient identity.

  1. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixUnit line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixUnit_star line 21
  3. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixUnit_mul line 25
  4. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixWordMonoid line 34
  5. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixWordMonoid_star line 50
  6. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixAlgebra_eq_span line 58