OAI/Analysis/Pureness/Quasitrace/QuasitraceNaturality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.starHomSelfAdjointMap line 11
2. lemma OAI.CuntzPureness.positiveMap_posPart line 19
3. lemma OAI.CuntzPureness.positiveMap_negPart line 26
4. lemma OAI.CuntzPureness.PositiveQuasitrace.selfAdjointValue_map line 36
5. theorem OAI.CuntzPureness.PositiveQuasitrace.complexValue_map line 42