OAI/Analysis/JiangSu/CentralSequences/TracialMatrixModelSaturation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectPacking.model_quotient_zero line 22
2. def OAI.DirectPacking.matrixModelEntry line 31
3. lemma OAI.DirectPacking.matrixModelEntry_apply line 36
4. lemma OAI.DirectPacking.matrixModel_star line 41
5. lemma OAI.DirectPacking.matrixModel_mul line 48
6. lemma OAI.DirectPacking.matrixModel_sum line 68
7. lemma OAI.DirectPacking.matrixModel_commute line 77
8. theorem OAI.DirectPacking.central_matrix_of_tracial_models line 85
9. theorem OAI.DirectComparison.comparison_central_matrix line 135