OAI/Analysis/Commutator/CFCTraceMoments.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.CFCTraceMoments.trace_cfc_of_powersline 23 - lemma
OAI.Kadison.CFCTraceMoments.trace_cyclic_powersline 64