OAI/Analysis/MatrixSigning/Complexity/PolynomialScalar.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_ratOp line 14
2. instance OAI.CurrentKS.Realization.poly_ratLE line 27
3. instance OAI.CurrentKS.Realization.poly_ratFloor line 38
4. instance OAI.CurrentKS.Realization.poly_conditional line 50
5. instance OAI.CurrentKS.Realization.poly_ite line 60
6. instance OAI.CurrentKS.Realization.poly_add line 62
7. instance OAI.CurrentKS.Realization.poly_sub line 63
8. instance OAI.CurrentKS.Realization.poly_mul line 64
9. instance OAI.CurrentKS.Realization.poly_div line 65
10. instance OAI.CurrentKS.Realization.poly_le line 66
11. instance OAI.CurrentKS.Realization.poly_neg line 67
12. instance OAI.CurrentKS.Realization.poly_abs line 68
13. instance OAI.CurrentKS.Realization.poly_roundScalar line 69