OAI/Analysis/MatrixSigning/Complexity/PolynomialRoutine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W23.NaturalPolynomial.comp line 10
2. lemma OAI.KS.W23.NaturalPolynomial.eval_comp line 16
3. class OAI.CurrentKS.Realization.PolyTime line 33
4. lemma OAI.CurrentKS.Realization.Realizes.output_length line 36
5. lemma OAI.CurrentKS.Realization.prodCode_length line 41
6. lemma OAI.CurrentKS.Realization.le_prodCode_left line 43
7. lemma OAI.CurrentKS.Realization.le_prodCode_right line 44
8. instance OAI.CurrentKS.Realization.poly_identity line 46
9. instance OAI.CurrentKS.Realization.poly_constant line 47
10. instance OAI.CurrentKS.Realization.poly_first line 49
11. instance OAI.CurrentKS.Realization.poly_second line 56
12. instance OAI.CurrentKS.Realization.poly_then line 62
13. instance OAI.CurrentKS.Realization.poly_both line 73
14. instance OAI.CurrentKS.Realization.poly_congr line 86
15. instance OAI.CurrentKS.Realization.poly_changeOutput line 91
16. instance OAI.CurrentKS.Realization.poly_reindex line 94