OAI/Analysis/TracialSplitting/PartitionAveraging.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearTrace.nuclear_uniform_finite_approximation line 20
2. lemma OAI.NuclearTrace.matrixSynthesis_scalarMatrixUnit line 58
3. lemma OAI.NuclearTrace.matrixSynthesis_map line 64
4. theorem OAI.NuclearTrace.nuclear_global_partition_averaging line 79