OAI/Analysis/Pureness/Quasitrace/QuasitraceFilteredQuotient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.boundedProductCStarAlgebra line 14
2. instance OAI.CuntzPureness.boundedProductPartialOrder line 16
3. instance OAI.CuntzPureness.boundedProductStarOrderedRing line 18
4. def OAI.CuntzPureness.filteredQuasitraceClosedIdeal line 25
5. abbrev OAI.CuntzPureness.FilteredQuasitraceQuotient line 30
6. def OAI.CuntzPureness.filteredQuasitraceQuotientMap line 32
7. lemma OAI.CuntzPureness.filteredQuasitraceQuotientMap_eq_zero line 35
8. lemma OAI.CuntzPureness.filteredQuasitraceQuotientMap_eq line 45
9. instance OAI.CuntzPureness.filteredQuasitraceQuotientNontrivial line 52
10. lemma OAI.CuntzPureness.filteredQuasitraceQuotient_norm_square line 61