OAI/Analysis/Commutator/MatrixCutEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.MatrixCorners.trace_reindex line 22
2. lemma OAI.Kadison.MatrixCorners.trace_cutBlock line 27
3. def OAI.Kadison.MatrixCorners.cutBlock line 31
4. def OAI.Kadison.MatrixCorners.reindexStarAlgEquiv line 42
5. def OAI.Kadison.MatrixCorners.cutEmbedding line 47
6. lemma OAI.Kadison.MatrixCorners.cutEmbedding_trace line 51
7. lemma OAI.Kadison.MatrixCorners.cutEmbedding_one line 57
8. def OAI.Kadison.MatrixCorners.projectionEmbedding line 78
9. lemma OAI.Kadison.MatrixCorners.projectionEmbedding_one line 84
10. lemma OAI.Kadison.MatrixCorners.projectionEmbedding_trace line 90