OAI/Analysis/MatrixSigning/Complexity/PolynomialOriginalOutput.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_appendBit line 12
2. instance OAI.CurrentKS.Realization.size_appendBit line 19
3. instance OAI.CurrentKS.Realization.poly_outputBits line 29
4. instance OAI.CurrentKS.Realization.poly_originalEmpty line 31
5. lemma OAI.CurrentKS.Realization.runsPoly_fullBody line 39
6. lemma OAI.CurrentKS.Realization.runsPoly_originalSigning line 54