In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that [...] x1+x2+⋯+xn−1+xn=−an−1an , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.
@article{bwmeta1.element.doi-10_1515_forma-2017-0008,
author = {Artur Korni\l owicz and Karol P\k ak},
title = {Vieta's Formula about the Sum of Roots of Polynomials},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {87-92},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0008}
}
Artur Korniłowicz; Karol Pąk. Vieta’s Formula about the Sum of Roots of Polynomials. Formalized Mathematics, Tome 25 (2017) pp. 87-92. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0008/