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.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The notion of a closed polynomial over a field of zero characteristic was introduced by Nowicki and Nagata. In this paper we discuss possible ways to define an analog of this notion over fields of positive characteristic. We are mostly interested in conditions of maximality of the algebra generated by a polynomial in a respective family of rings. We also present a modification of the condition of integral closure and discuss a condition involving partial derivatives.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The notion of the characteristic of rings and its basic properties are formalized [14], [39], [20]. Classification of prime fields in terms of isomorphisms with appropriate fields (ℚ or ℤ/p) are presented. To facilitate reasonings within the field of rational numbers, values of numerators and denominators of basic operations over rationals are computed.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.