OAI/Analysis/FreeWords/MatrixProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KKMatrixQuantization.productUnits line 22
2. theorem OAI.KKMatrixQuantization.productUnits_mul line 26
3. theorem OAI.KKMatrixQuantization.productUnits_one line 41
4. theorem OAI.KKMatrixQuantization.productUnits_star line 46
5. def OAI.KKMatrixQuantization.matrixProduct line 50
6. theorem OAI.KKMatrixQuantization.matrixProduct_unit line 54
7. theorem OAI.KKMatrixQuantization.matrixProduct_average line 60