OAI/Analysis/Commutator/FiniteFactorTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.OrbitStateHull.hull_projectionContinuousAtOne line 32
2. theorem OAI.Kadison.OrbitStateHull.hull_norm_separable line 38
3. theorem OAI.Kadison.OrbitStateHull.hull_normal line 45
4. theorem OAI.Kadison.OrbitStateHull.exists_faithful_normal_trace line 50