OAI/Analysis/Nuclearity/QuotientTensorNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensor-norm nuclearity of a separable quotient of the nuclear source. The completion is made unital using the image of its algebraic unit; no unital representation of the quotient in a nonunital algebra is assumed.

  1. def OAI.WeakPureInfiniteness.algebraicLeft line 22
  2. def OAI.WeakPureInfiniteness.algebraicRight line 26
  3. lemma OAI.WeakPureInfiniteness.algebraic_legs line 32
  4. lemma OAI.WeakPureInfiniteness.algebraic_legs_commute line 39
  5. lemma OAI.WeakPureInfiniteness.quotient_dense_tensor_norm line 44
  6. lemma OAI.WeakPureInfiniteness.quotient_norm_value line 83
  7. theorem OAI.WeakPureInfiniteness.nuclear_quotient_tensorNorm line 99