OAI/Analysis/KadisonSimilarity/Tracial/SourceConstantMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Prescribed-source unitaries annihilate all centered constant mixed moments.

  1. theorem OAI.KadisonSimilarity.exists_source_constant_integer_moments line 34