OAI/Analysis/Pureness/Stabilization/MatrixInterleaveSystem.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.finProdFinEquiv_cast line 11
2. theorem OAI.CuntzTrace.matrixInterleave_inclusion line 16
3. def OAI.CuntzTrace.matrixLimitBlock line 45
4. theorem OAI.CuntzTrace.matrixLimitBlock_norm line 48
5. theorem OAI.CuntzTrace.matrixLimitBlock_compatible line 53