OAI/Analysis/JiangSu/CuntzSemigroup/PositiveQuasitrace.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Pureness.PositiveQuasitrace line 13
2. instance OAI.Pureness.(instance at line 22) line 22
3. def OAI.Pureness.finiteSpectralPositiveQuasitrace line 27
4. lemma OAI.Pureness.finiteSpectralPositiveQuasitrace_inclusion line 44
5. lemma OAI.Pureness.finiteSpectralPositiveQuasitrace_root_rank line 52
6. lemma OAI.Pureness.commute_posPart_left line 77
7. lemma OAI.Pureness.commute_negPart_left line 79
8. lemma OAI.Pureness.commute_posPart_right line 81
9. lemma OAI.Pureness.commute_negPart_right line 83
10. def OAI.Pureness.PositiveQuasitrace.selfAdjointValue line 88
11. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_sub line 91
12. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_add line 106
13. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_smul_nonneg line 125
14. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_neg line 137
15. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_smul line 143
16. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_positive line 152
17. lemma OAI.Pureness.PositiveQuasitrace.selfAdjointValue_zero line 158
18. def OAI.Pureness.PositiveQuasitrace.complexValue line 175
19. lemma OAI.Pureness.PositiveQuasitrace.complexValue_selfAdjoint line 178
20. lemma OAI.Pureness.PositiveQuasitrace.complexValue_positive line 183
21. lemma OAI.Pureness.PositiveQuasitrace.complexValue_polar line 186
22. lemma OAI.Pureness.PositiveQuasitrace.complexValue_square_nonneg line 190
23. lemma OAI.Pureness.PositiveQuasitrace.complexValue_real_add_I line 195
24. def OAI.Pureness.PositiveQuasitrace.subalgebraSelfAdjointMap line 207
25. def OAI.Pureness.PositiveQuasitrace.subalgebraRealLinear line 212
26. def OAI.Pureness.PositiveQuasitrace.subalgebraComplexLinear line 221
27. lemma OAI.Pureness.PositiveQuasitrace.subalgebraComplexLinear_eq line 229