In this article we further extend the algebraic theory of polynomial rings in Mizar [1, 2, 3]. We deal with roots and multiple roots of polynomials and show that both the real numbers and finite domains are not algebraically closed [5, 7]. We also prove the identity theorem for polynomials and that the number of multiple roots is bounded by the polynomial’s degree [4, 6].
@article{bwmeta1.element.doi-10_1515_forma-2017-0018,
author = {Christoph Schwarzweller},
title = {On Roots of Polynomials and Algebraically Closed Fields},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {185-195},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0018}
}
Christoph Schwarzweller. On Roots of Polynomials and Algebraically Closed Fields. Formalized Mathematics, Tome 25 (2017) pp. 185-195. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0018/