OAI/Analysis/KadisonKastler/TracialVectorExistence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Realizing the finite-factor trace by a vector in the given representation

  1. theorem OAI.KadisonKastler.exists_tracial_vector_of_II1_cyclic line 19
  2. theorem OAI.KadisonKastler.exists_tracial_vector_of_II1_separating line 54