OAI/Analysis/MatrixSigning/Complexity/PolynomialMatrixSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.addMatrices line 12
2. lemma OAI.CurrentKS.Realization.matrixAdd_shape line 13
3. lemma OAI.CurrentKS.Realization.matrixAdd_parts line 21
4. lemma OAI.CurrentKS.Realization.matrixAdd_fold line 27
5. instance OAI.CurrentKS.Realization.size_matrixAdd line 36