OAI/Analysis/Pureness/Comparison/TracialExtendedTrace.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CuntzComparison.TracialState.extendedTraceline 12 - lemma
OAI.CuntzComparison.TracialState.extendedTrace_applyline 37 - theorem
OAI.CuntzComparison.TracialState.extended_matrixTraceline 40