OAI/Analysis/JiangSu/Nuclearity/NuclearCommutingExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.IsNuclear.tensorCompletionEquiv line 16
2. lemma OAI.Pureness.IsNuclear.tensorCompletionEquiv_tensor line 24
3. lemma OAI.Pureness.IsNuclear.tensorCompletionEquiv_norm line 32
4. def OAI.CStarAbsorption.nuclearCommutingHom line 56
5. theorem OAI.CStarAbsorption.nuclearCommutingHom_tensor line 62
6. theorem OAI.CStarAbsorption.nuclearCommutingHom_commute line 70