OAI/Analysis/Pureness/Quasitrace/QuasitraceSelfAdjoint.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.commute_posPart_left line 10
2. lemma OAI.CuntzPureness.commute_negPart_left line 11
3. lemma OAI.CuntzPureness.commute_posPart_right line 12
4. lemma OAI.CuntzPureness.commute_negPart_right line 13
5. def OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue line 19
6. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_sub line 22
7. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_add line 37
8. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_smul_nonneg line 56
9. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_neg line 68
10. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_smul line 74
11. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_positive line 83
12. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_zero line 89