OAI/Analysis/FreeWords/MatrixHilbertCore.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KKMatrixHilbert.matrixOperator_add line 19
2. theorem OAI.KKMatrixHilbert.matrixOperator_mul line 25
3. theorem OAI.KKMatrixHilbert.matrixOperator_one line 33
4. theorem OAI.KKMatrixHilbert.matrixOperator_star line 41
5. def OAI.KKMatrixHilbert.matrixOperatorHom line 49
6. theorem OAI.KKMatrixHilbert.matrixOperator_diagonal_apply line 66
7. theorem OAI.KKMatrixHilbert.norm_diagonal_le line 75