OAI/Analysis/TracialSplitting/TensorExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.denseStarCompletionHom line 23
2. lemma OAI.Pureness.denseStarCompletionHom_apply line 53
3. lemma OAI.Pureness.denseStarCompletionHom_unique line 58
4. lemma OAI.Pureness.denseStarCompletionHom_denseRange line 66
5. theorem OAI.Pureness.IsNuclear.representation_norm_le line 80
6. def OAI.Pureness.IsNuclear.extendRepresentation line 94
7. lemma OAI.Pureness.IsNuclear.extendRepresentation_apply line 100