OAI/Analysis/Nuclearity/UnitalMinimalTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The unit and the two unital legs of a minimal tensor product. The unital structure is exposed as a definition for local use in the factor argument.

  1. theorem OAI.WeakPureInfiniteness.minimalTensor_unit_left line 14
  2. theorem OAI.WeakPureInfiniteness.minimalTensor_unit_right line 30
  3. abbrev OAI.WeakPureInfiniteness.minimalTensorUnitalStructure line 46
  4. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.one_eq line 56
  5. def OAI.WeakPureInfiniteness.UnitalMinimalTensor.leftEmbedding line 61
  6. def OAI.WeakPureInfiniteness.UnitalMinimalTensor.rightEmbedding line 71
  7. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.legs_mul line 85
  8. theorem OAI.WeakPureInfiniteness.UnitalMinimalTensor.legs_commute line 90