OAI/Analysis/KadisonSimilarity/Tracial/SourceAllMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All mixed words from a countable ambient family vanish for a sequence of source unitaries in the tracial ultrapower.

  1. theorem OAI.KadisonSimilarity.exists_source_quotient_unitary_all_moments line 35