<abstract xmlns="http://www.w3.org/1999/xhtml">In the article we formalized in the Mizar system [<xref ref-type="bibr" rid="j_forma-2017-0008_ref_002_w2aab3b7ab1b6b1ab1ab2Aa">2</xref>] the Vieta formula about the sum of roots of a polynomial <italic>anxn</italic> + <italic>an−</italic>1<italic>xn−</italic>1 + <italic>···</italic> + <italic>a</italic>1<italic>x</italic> + <italic>a</italic>0 defined over an algebraically closed field. The formula says that 
<inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2017-0008_eq_001.png"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><msub><mi>x</mi><mn>1</mn></msub><mo>+</mo><msub><mi>x</mi><mn>2</mn></msub><mo>+</mo><mo>⋯</mo><mo>+</mo><msub><mi>x</mi><mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>+</mo><msub><mi>x</mi><mi>n</mi></msub><mo>=</mo><mo>−</mo><mfrac><mrow><msub><mi>a</mi><mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub></mrow><mrow><msub><mi>a</mi><mi>n</mi></msub></mrow></mfrac></mrow></math><tex-math>$x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$</tex-math></alternatives></inline-formula>
, where <italic>x</italic>1, <italic>x</italic>2,…, <italic>xn</italic> are (not necessarily distinct) roots of the polynomial [<xref ref-type="bibr" rid="j_forma-2017-0008_ref_012_w2aab3b7ab1b6b1ab1ac12Aa">12</xref>]. In the article the sum is denoted by <monospace>SumRoots</monospace>.</abstract>

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$x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$
, where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.

Vieta’s Formula about the Sum of Roots of Polynomials

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Vieta\u2019s Formula about the Sum of Roots of Polynomials"}

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...

Vieta’s Formula about the Sum of Roots of Polynomials

Published Online: Sep 23, 2017

Page range: 87 - 92

Received: May 25, 2017

DOI: https://doi.org/10.1515/forma-2017-0008

Keywords
roots of polynomials, Vieta’s formula

© 2017 Artur Korniłowicz et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Vieta’s Formula about the Sum of Roots of Polynomials

Published Online: Sep 23, 2017

Page range: 87 - 92

Received: May 25, 2017

DOI: https://doi.org/10.1515/forma-2017-0008

Keywordsroots of polynomials, Vieta’s formula

© 2017 Artur Korniłowicz et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Keywords
roots of polynomials, Vieta’s formula