OAI/Analysis/JiangSu/TensorProducts/CommutingStarTensor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Pureness.commutingStarTensorHom_injective line 18
  2. abbrev OAI.Pureness.commutingTensorNormedRing line 28
  3. abbrev OAI.Pureness.commutingTensorNormedAlgebra line 32
  4. theorem OAI.Pureness.commutingTensorCStarRing line 39
  5. lemma OAI.Pureness.commutingTensor_norm_def line 48
  6. lemma OAI.Pureness.commutingTensor_norm_tmul_le line 52
  7. def OAI.Pureness.commutingTensorClosureMap line 67
  8. lemma OAI.Pureness.commutingTensorClosureMap_coe line 71
  9. lemma OAI.Pureness.commutingTensorClosureMap_injective line 74
  10. lemma OAI.Pureness.commutingTensorClosureMap_denseRange line 80
  11. lemma OAI.Pureness.commutingTensorClosureMap_isometry line 90
  12. lemma OAI.Pureness.commutingTensorClosure_eq_generated line 99
  13. def OAI.Pureness.denseStarCompletionLinearEquiv line 131
  14. lemma OAI.Pureness.denseStarCompletionLinearEquiv_apply line 134
  15. def OAI.Pureness.denseStarCompletionEquiv line 138
  16. lemma OAI.Pureness.denseStarCompletionEquiv_apply line 159
  17. lemma OAI.Pureness.denseStarCompletionEquiv_norm line 163