OAI/Analysis/Pureness/Quasitrace/QuasitraceQuotientNorm.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.PositiveQuasitrace.nullSequenceSubmodule line 13
2. lemma OAI.CuntzPureness.PositiveQuasitrace.nullSequenceSubmodule_coe line 16
3. instance OAI.CuntzPureness.PositiveQuasitrace.nullSequenceSubmodule_closed line 24
4. def OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientLinearEquiv line 28
5. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientLinearEquiv_mk line 32
6. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormedAddCommGroup line 35
7. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormedSpace line 39
8. def OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormEquiv line 42
9. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientMap_norm_le line 47
10. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotient_norm_lt_rep line 53
11. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientCompleteSpace line 60
12. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotient_norm_mul_le line 63
13. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormedRing line 81
14. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormedAlgebra line 85
15. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotient_norm_star line 88
16. instance OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientNormedStarGroup line 97
17. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchyQuotientStarHom_continuous line 100