OAI/Analysis/JiangSu/CentralSequences/UnitalNormCentralAlgebra.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectComparison.unitalNormCentralizer line 24
2. instance OAI.DirectComparison.unitalNormCentralizer_closed line 37
3. instance OAI.DirectComparison.(instance at line 42) line 42
4. instance OAI.DirectComparison.(instance at line 45) line 45
5. instance OAI.DirectComparison.(instance at line 46) line 46
6. instance OAI.DirectComparison.(instance at line 47) line 47
7. instance OAI.DirectComparison.(instance at line 48) line 48
8. def OAI.DirectComparison.normToTracialUnital line 50
9. def OAI.DirectComparison.unitalCentralToTracial line 57
10. lemma OAI.DirectComparison.unitalNormCentralizer_nonneg_iff line 61
11. theorem OAI.DirectComparison.unitalNormCentralizer_sigma line 76
12. theorem OAI.DirectComparison.unital_central_surjective line 114
13. theorem OAI.DirectComparison.unital_central_matrix_lift line 137
14. theorem OAI.DirectComparison.comparison_central_order_zero line 154