OAI/Analysis/Pureness/Stabilization/MatrixSystem.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.matrixPad line 9
2. lemma OAI.CuntzTrace.matrixPad_self line 12
3. lemma OAI.CuntzTrace.matrixPad_succ line 14
4. lemma OAI.CuntzTrace.matrixPad_trans line 17
5. def OAI.CuntzTrace.matrixInclusion line 21
6. lemma OAI.CuntzTrace.matrixInclusion_norm line 48
7. lemma OAI.CuntzTrace.matrixInclusion_isometry line 55
8. lemma OAI.CuntzTrace.matrixInclusion_trans line 61