OAI/Analysis/JiangSu/CStarAlgebras/CStarNormCompletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.CStarAlgebraNorm.completionMap line 21
2. lemma OAI.Pureness.CStarAlgebraNorm.completionMap_norm line 37
3. lemma OAI.Pureness.CStarAlgebraNorm.completionMap_injective line 44
4. theorem OAI.Pureness.CStarAlgebraNorm.eq_original line 54
5. theorem OAI.Pureness.CStarAlgebraNorm.le_of_bound line 66
6. theorem OAI.Pureness.CStarAlgebraNorm.eq_of_mutual_bound line 95