OAI/Analysis/Pureness/Completion/NonUnitalCStarCompletion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.nonUnitalCompletionMul line 12
2. lemma OAI.CuntzPureness.completion_coe_mul line 18
3. instance OAI.CuntzPureness.nonUnitalCompletionContinuousMul line 23
4. instance OAI.CuntzPureness.nonUnitalCompletionNonUnitalRing line 31
5. instance OAI.CuntzPureness.nonUnitalCompletionNonUnitalNormedRing line 44
6. instance OAI.CuntzPureness.nonUnitalCompletionStar line 50
7. lemma OAI.CuntzPureness.completion_coe_star line 53
8. instance OAI.CuntzPureness.nonUnitalCompletionContinuousStar line 57
9. instance OAI.CuntzPureness.nonUnitalCompletionStarRing line 60
10. instance OAI.CuntzPureness.nonUnitalCompletionCStarRing line 68
11. instance OAI.CuntzPureness.nonUnitalCompletionStarModule line 73
12. instance OAI.CuntzPureness.nonUnitalCompletionScalarTower line 79
13. instance OAI.CuntzPureness.nonUnitalCompletionSMulComm line 87
14. instance OAI.CuntzPureness.nonUnitalCompletionCStarAlgebra line 95