OAI/Analysis/Commutator/MatrixTraceFaithful.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.MatrixGNS.algebraArray_eq_zero_iffline 25 - lemma
OAI.Kadison.MatrixGNS.trace_faithfulline 39 - lemma
OAI.Kadison.MatrixGNS.balanced_symmetry_trace_zeroline 52