OAI/Analysis/TracialSplitting/NuclearTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Pureness.NuclearLift.(instance at line 20) line 20
2. instance OAI.Pureness.NuclearLift.(instance at line 22) line 22
3. instance OAI.Pureness.NuclearLift.(instance at line 27) line 27
4. instance OAI.Pureness.NuclearLift.(instance at line 30) line 30
5. instance OAI.Pureness.NuclearLift.(instance at line 33) line 33
6. def OAI.Pureness.CStarAlgebraNorm.comapEquiv line 42
7. lemma OAI.Pureness.CStarAlgebraNorm.comapEquiv_injective line 55
8. theorem OAI.Pureness.IsNuclear.small line 72