OAI/Analysis/BoundedHochschild/PaulsenSystem.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unital two-by-two operator system associated to a linear map.

  1. def OAI.BoundedHochschild.KadisonRingrose.starConjugateLinear line 16
  2. def OAI.BoundedHochschild.KadisonRingrose.paulsenSystem line 21
  3. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenSystem_one line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenSystem_star line 37
  5. def OAI.BoundedHochschild.KadisonRingrose.paulsenLinear line 48
  6. def OAI.BoundedHochschild.KadisonRingrose.paulsenSystemMap line 59
  7. lemma OAI.BoundedHochschild.KadisonRingrose.paulsenSystemMap_one line 62