OAI/Analysis/Nuclearity/MinimalTensorAlgebraic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The algebraic tensor product embeds faithfully and densely in the minimal C*-completion.

  1. def OAI.WeakPureInfiniteness.UnitalMinimalTensor.algebraicMap line 20
  2. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.algebraicMap_tmul line 23
  3. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.algebraicMap_injective line 26
  4. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.algebraicMap_dense line 54