OAI/Analysis/Nuclearity/MinimalTensorExtension.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Extension from the dense algebraic tensor product, with a nonunital target. An auxiliary unital structure gives extensions to concrete represented subalgebras.

  1. def OAI.WeakPureInfiniteness.nonUnitalStarLinearMap line 19
  2. def OAI.WeakPureInfiniteness.denseNonUnitalStarCompletion line 24
  3. lemma OAI.WeakPureInfiniteness.denseNonUnitalStarCompletion_apply line 50
  4. def OAI.WeakPureInfiniteness.denseLinearStarCompletion line 64
  5. lemma OAI.WeakPureInfiniteness.denseLinearStarCompletion_apply line 90
  6. def OAI.WeakPureInfiniteness.minimalTensorBilinear line 104
  7. def OAI.WeakPureInfiniteness.minimalAlgebraicLinear line 115
  8. lemma OAI.WeakPureInfiniteness.minimalAlgebraicLinear_tmul line 118
  9. lemma OAI.WeakPureInfiniteness.minimalAlgebraicLinear_dense line 121
  10. lemma OAI.WeakPureInfiniteness.algebraic_linear_norm_le line 134
  11. def OAI.WeakPureInfiniteness.minimalAlgebraicMap line 148
  12. lemma OAI.WeakPureInfiniteness.minimalAlgebraicMap_tmul line 168
  13. lemma OAI.WeakPureInfiniteness.minimalAlgebraicMap_dense line 173
  14. lemma OAI.WeakPureInfiniteness.minimalAlgebraicMap_apply line 177
  15. lemma OAI.WeakPureInfiniteness.minimalAlgebraicLinear_mul line 182
  16. lemma OAI.WeakPureInfiniteness.minimalAlgebraicLinear_star line 186
  17. def OAI.WeakPureInfiniteness.minimalTensorExtend line 190
  18. lemma OAI.WeakPureInfiniteness.minimalTensorExtend_apply line 196
  19. lemma OAI.WeakPureInfiniteness.minimalTensorExtend_elementary line 202