OAI/Analysis/Pureness/Operators/FiniteRegularMatrixModel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.permutationCStarUnitary line 14
2. def OAI.CuntzPureness.finiteRegularMatrix line 34
3. lemma OAI.CuntzPureness.finiteRegularMatrix_norm line 38
4. lemma OAI.CuntzPureness.finiteRegularMatrix_entry line 41
5. theorem OAI.CuntzPureness.finiteRegularMatrix_trace line 45
6. instance OAI.CuntzPureness.separatingQuotient_fintype line 64
7. def OAI.CuntzPureness.separatingMatrixModel line 67
8. lemma OAI.CuntzPureness.separatingMatrixModel_norm line 71
9. theorem OAI.CuntzPureness.separatingMatrixModel_trace_eventually line 75