OAI/Analysis/Pureness/States/QuotientGenuineQuasitrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveQuasitrace.quotientPositiveQuasitrace line 14
2. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientPositiveQuasitrace_selfAdjointValue line 24
3. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientPositiveQuasitrace_complexValue line 33
4. def OAI.CuntzPureness.PositiveQuasitrace.quotientComplexQuasitrace line 42
5. lemma OAI.CuntzPureness.PositiveQuasitrace.quotientComplexQuasitrace_eq line 45