OAI/Analysis/KadisonSimilarity/FreeProduct/NormalInclusionFreeness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The free-position specialization from normal trace models and closed source trace balls. No predual construction for a matrix algebra is needed.

  1. theorem OAI.KadisonSimilarity.popa1995_of_normal_traces line 18