OAI/Analysis/Pureness/Stabilization/MatrixAdditionComm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.matrixSwapPermutation line 10
2. lemma OAI.CuntzTrace.matrixSwapPermutation_apply line 13
3. theorem OAI.CuntzTrace.matrixInterleave_swap line 18
4. def OAI.CuntzTrace.matrixBlockSwapHom line 29
5. lemma OAI.CuntzTrace.matrixBlockPositive_stage line 32
6. theorem OAI.CuntzTrace.matrixBlockPositive_comm line 37
7. theorem OAI.CuntzTrace.CuntzClass.matrixAdd_comm line 56