OAI/Analysis/OperatorAlgebra/TracialTensorCompletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Completion of a tracial tensor representation that is continuous for the minimal tensor norm.

  1. lemma OAI.WeakPureInfiniteness.tracialTensorAlgebraic_mul line 19
  2. lemma OAI.WeakPureInfiniteness.tracialTensorAlgebraic_star line 31
  3. def OAI.WeakPureInfiniteness.tracialTensorMinimal line 38
  4. lemma OAI.WeakPureInfiniteness.tracialTensorMinimal_algebraic line 45
  5. lemma OAI.WeakPureInfiniteness.traceTensor_elementary line 50
  6. lemma OAI.WeakPureInfiniteness.tracialTensorMinimal_elementary line 56