Differentiability of Polynomials over Reals
Artur Korniłowicz
Formalized Mathematics, Tome 25 (2017), p. 31-37 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].

Publié le : 2017-01-01
EUDML-ID : urn:eudml:doc:288126 
@article{bwmeta1.element.doi-10_1515_forma-2017-0002,
     author = {Artur Korni\l owicz},
     title = {Differentiability of Polynomials over Reals},
     journal = {Formalized Mathematics},
     volume = {25},
     year = {2017},
     pages = {31-37},
     zbl = {06726493},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0002}
}

Artur Korniłowicz. Differentiability of Polynomials over Reals. Formalized Mathematics, Tome 25 (2017) pp. 31-37. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0002/