OAI/Analysis/Pureness/Quasitrace/QuasitraceComplex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.complexValue line 12
2. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_selfAdjoint line 15
3. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_positive line 20
4. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_polar line 23
5. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_square_nonneg line 27
6. lemma OAI.CuntzPureness.PositiveQuasitrace.complexValue_real_add_I line 32
7. def OAI.CuntzPureness.PositiveQuasitrace.subalgebraSelfAdjointMap line 44
8. def OAI.CuntzPureness.PositiveQuasitrace.subalgebraRealLinear line 49
9. def OAI.CuntzPureness.PositiveQuasitrace.subalgebraComplexLinear line 58
10. lemma OAI.CuntzPureness.PositiveQuasitrace.subalgebraComplexLinear_eq line 66