OAI/Analysis/KadisonKastler/NormalizedPolarPath.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Based approximate-normalizer paths from smoothed algebra relations
- theorem
OAI.KadisonKastler.exists_based_polar_normalizer_pathline 19