OAI/Analysis/Nuclearity/TensorMultiplierAction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The unital right factor acts on a nonunital minimal tensor product

  1. lemma OAI.WeakPureInfiniteness.spatialRight_zero line 16
  2. lemma OAI.WeakPureInfiniteness.spatialRight_add line 19
  3. lemma OAI.WeakPureInfiniteness.spatialRight_mul line 23
  4. lemma OAI.WeakPureInfiniteness.spatialRight_smul line 27
  5. lemma OAI.WeakPureInfiniteness.spatialRight_star line 31
  6. def OAI.WeakPureInfiniteness.tensorRightAction line 35
  7. def OAI.WeakPureInfiniteness.tensorLeftAction line 47
  8. lemma OAI.WeakPureInfiniteness.tensorRightAction_val line 61
  9. lemma OAI.WeakPureInfiniteness.tensorLeftAction_val line 64
  10. lemma OAI.WeakPureInfiniteness.tensorRightAction_elementary line 69
  11. lemma OAI.WeakPureInfiniteness.tensorLeftAction_elementary line 73
  12. lemma OAI.WeakPureInfiniteness.tensorRightAction_one line 79
  13. lemma OAI.WeakPureInfiniteness.tensorLeftAction_one line 87
  14. def OAI.WeakPureInfiniteness.tensorRightFactorMultiplier line 91
  15. def OAI.WeakPureInfiniteness.tensorRightFactorHom line 100
  16. lemma OAI.WeakPureInfiniteness.coe_mul_tensorRightFactor line 157
  17. lemma OAI.WeakPureInfiniteness.tensorRightFactor_mul_coe line 168
  18. lemma OAI.WeakPureInfiniteness.tensorMultiplier_coefficient line 179
  19. lemma OAI.WeakPureInfiniteness.tensorMultiplier_commute line 186