OAI/Analysis/Pureness/Stabilization/MatrixEmbedding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.matrixEmbedding_size line 10
2. def OAI.CuntzTrace.matrixEmbeddingPermutation line 13
3. lemma OAI.CuntzTrace.matrixEmbeddingPermutation_apply line 17
4. def OAI.CuntzTrace.matrixEmbedding line 22
5. theorem OAI.CuntzTrace.matrixEmbedding_entry line 25
6. theorem OAI.CuntzTrace.matrixEmbedding_outside line 31
7. theorem OAI.CuntzTrace.matrixEmbedding_ext line 45
8. theorem OAI.CuntzTrace.matrixEmbedding_cuntzClass line 60