OAI/Analysis/OperatorAlgebra/StandardMinimalMultiplication.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The standard left/right multiplication representation extends to the minimal tensor product for a represented quotient of a nuclear algebra.

  1. def OAI.WeakPureInfiniteness.standardRightHom line 19
  2. lemma OAI.WeakPureInfiniteness.standardRightHom_apply line 23
  3. lemma OAI.WeakPureInfiniteness.standardLeftRight_commute line 26
  4. def OAI.WeakPureInfiniteness.standardAlgebraicMultiplication line 31
  5. lemma OAI.WeakPureInfiniteness.standardAlgebraicMultiplication_tmul line 36
  6. def OAI.WeakPureInfiniteness.standardAlgebraicLinear line 43
  7. lemma OAI.WeakPureInfiniteness.standardAlgebraicLinear_apply line 49
  8. lemma OAI.WeakPureInfiniteness.nuclear_quotient_standard_finite_bound line 56
  9. lemma OAI.WeakPureInfiniteness.nuclear_quotient_standard_algebraic_bound line 70
  10. lemma OAI.WeakPureInfiniteness.subalgebraAlgebraicLinear_mul line 83
  11. lemma OAI.WeakPureInfiniteness.subalgebraAlgebraicLinear_star line 95
  12. def OAI.WeakPureInfiniteness.nuclearQuotientStandardMultiplication line 103