OAI/Analysis/Pureness/Tensor/CommutingTensorClosure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.commutingTensorClosure line 12
2. instance OAI.CuntzPureness.commutingTensorClosure_closed line 15
3. instance OAI.CuntzPureness.commutingTensorClosureCStarAlgebra line 18
4. def OAI.CuntzPureness.commutingTensorClosureMap line 21
5. lemma OAI.CuntzPureness.commutingTensorClosureMap_coe line 25
6. lemma OAI.CuntzPureness.commutingTensorClosureMap_injective line 28
7. lemma OAI.CuntzPureness.commutingTensorClosureMap_denseRange line 34
8. lemma OAI.CuntzPureness.commutingTensorClosureMap_isometry line 44
9. lemma OAI.CuntzPureness.commutingTensorClosure_eq_generated line 53