Differentiability of polynomials over reals

DOI10.1515/FORMA-2017-0002MaRDI QIDQ2356935zbMATH OpenOpenAlexFDO

Authors Artur Korniłowicz

Publication date 7 June 2017

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 3.0 Unported

Full work available at URL https://doi.org/10.1515/forma-2017-0002

zbMATH Keywords

derivative of real polynomialsdifferentiation of real polynomials

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Differentiation (real functions of one variable): general theory, generalized derivatives, mean value theorems (26A24)

Recommendations

• Defining power series and polynomials in Mizar
• The Arithmetic of Differentiation
• Differentiation in normed spaces
• On roots of polynomials and algebraically closed fields
• Higher-order partial differentiation

Cites work

• Four decades of \textsc{Mizar}. Foreword
• scientific article; zbMATH DE number 3195516 (Why is no real title available?)
• Semantics of MML query -- ordering

Cited in

(5)

• Derivation of commutative rings and the Leibniz formula for power of derivation
• Gâteaux differentiability of polynomial test and generalized functions
• Norm-attaining polynomials and differentiability
• Differentiation on interval
• Formal proof of transcendence of the number e. I

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Differentiability of polynomials over reals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2356935)