OAI/Analysis/Pureness/Traces/TracialStates.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.CuntzPureness.TracialStateline 9 - theorem
OAI.CuntzPureness.TracialState.conjugate_leline 16 - theorem
OAI.CuntzPureness.TracialState.faithfulline 36 - theorem
OAI.CuntzPureness.TracialState.map_eq_zero_iffline 49