Polynomials and power series

AbbreviationPolynomial in one indeterminate#

A polynomial in one indeterminate over a ring \(R\) is a formal expression \(a_0 + a_1 X + \dots + a_n X^n\) with coefficients \(a_i\) in \(R\), added and multiplied by the familiar rules of high-school algebra. The polynomials over \(R\) form a ring \(R[X]\), the polynomial ring. It is the simplest way to enlarge a ring by one new element, and it underlies much of algebra: the theory of equations, field extensions, algebraic geometry and the study of linear maps through their characteristic polynomials.

Definition

Let \(R\) be a ring. A polynomial over \(R\) is a sequence \((a_0, a_1, a_2, \dots)\) of elements of \(R\) in which only finitely many terms are nonzero, that is, a finitely supported function from the natural numbers to \(R\). The term \(a_n\) is the coefficient of \(X^n\), and two polynomials are equal exactly when all their coefficients agree. Addition is coefficientwise, and multiplication is defined so that \(X^i X^j = X^{i+j}\): the product of \(f = \sum_i a_i X^i\) and \(g = \sum_j b_j X^j\) has as coefficient of \(X^n\) the sum of \(a_i b_j\) over all pairs with \(i + j = n\),

\[fg = \sum_{n \ge 0} \Bigl( \sum_{i+j=n} a_i b_j \Bigr) X^n.\]

The indeterminate \(X\) is the sequence \((0, 1, 0, 0, \dots)\), and an element \(a\) of \(R\) is identified with the constant polynomial \((a, 0, 0, \dots)\). With these identifications every polynomial is the finite sum of its terms \(a_i X^i\), which justifies the usual notation. Even when \(R\) is not commutative, \(X\) commutes with every polynomial.

The degree of a nonzero polynomial \(f\) is the largest \(n\) with \(a_n \neq 0\), and \(a_n\) is its leading coefficient; \(f\) is monic if its leading coefficient is \(1\). The zero polynomial has no nonzero coefficient, and its degree is set to \(-\infty\).

When \(R\) is commutative, a polynomial \(f = a_0 + a_1 X + \dots + a_n X^n\) can be evaluated at an element \(x\) of \(R\): its value is \(f(x) = a_0 + a_1 x + \dots + a_n x^n\), and \(x\) is a root of \(f\) when \(f(x) = 0\).

Examples
Properties

Iterating the construction, or allowing any set of indeterminates, gives polynomials in several indeterminates; dropping the finiteness condition on the coefficients gives formal power series. Within \(R[X]\) one studies irreducible polynomials, with tests such as Eisenstein's criterion, the formal derivative and separable polynomials. Quotients of \(K[X]\) by an irreducible polynomial build field extensions, as in the rupture field and the splitting field.

In Mathlib

Mathlib defines polynomials over any semiring, commutative or not, so that the natural numbers and other semirings without subtraction are allowed as coefficients; results that need negatives, commutativity or the absence of zero divisors carry those as hypotheses. A polynomial is stored as a finitely supported function from the natural numbers to the coefficients, wrapped in its own structure so that it is used only through its own interface; the constant polynomials come from a ring morphism from \(R\) into \(R[X]\), and \(X\) is a separate element. Mathlib has two notions of degree: one with values in the natural numbers extended by a bottom element, where the zero polynomial has degree bottom, playing the role of \(-\infty\), and one with natural-number values, where the zero polynomial has degree \(0\). The bound on the number of roots appears in both forms: with the first for nonzero polynomials, and with the second for all polynomials, the zero polynomial included, since Mathlib assigns it no roots. Division by a monic polynomial is defined for every divisor, monic or not, and the identity \(f = gq + r\) holds in all cases, with a quotient of zero when the divisor is not monic; only the degree bound on the remainder needs a monic divisor and a nonzero ring. Over a field, a separate division operation divides by any nonzero polynomial.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial
Uses 2 · Used by 36
Statement usesRing · Finitely supported function
Used byDirichlet unit theorem · Algebraic extension · Algebraically closed field · \(\C\) is algebraically closed · Existence of algebraic closure of a field · Rupture field · Splitting field · Hensel's lemma (for \(\mathbb{Z}_p\)) · \(A[X]\) has gcd and lcm if \(A\) does · \(A[{X_i}]\) is a UFD when \(A\) is a UFD · Eisenstein's criterion · Hilbert basis theorem · \(K[X]\) is Euclidean · Multiplicity · Power series · Roots of a polynomial · Separable polynomial · Liouville's theorem on existence of transcendental numbers · Characteristic polynomial · Minimal polynomial · Structure theorem · Integral root theorem · Rational root theorem · Going-up and going-down theorems · Krull's principal ideal theorem · Vieta's formulas · Dirichlet's unit theorem · Mahler's theorem · Annihilating polynomials · Lagrange interpolation · Algebraic elements · Rational fraction fields with one indeterminate over a field · Polynomial derivative · Polynomial functions · Taylor's theorem with integral form for remainder (Taylor-like theorems) · Taylor's theorem with Lagrange form for remainder

DefinitionRoots of a polynomial#

The roots of a polynomial \(p\) are the values \(a\) at which the polynomial vanishes, that is, \(p(a) = 0\). Over an integral domain, the roots of a nonzero polynomial, each counted as often as its multiplicity, form a finite multiset whose size is at most the degree of \(p\). Roots tie the evaluation of a polynomial to its factorization: finding the roots of \(p\) is the same as finding its factors of the form \(X - a\), and this link underlies the solution of equations, the theory of field extensions, and the fact that a polynomial of small degree is determined by few of its values.

Definition

Let \(R\) be an integral domain: a commutative ring with \(1 \neq 0\) in which a product of nonzero elements is nonzero. An element \(a \in R\) is a root of \(p \in R[X]\) when \(p(a) = 0\). By the factor theorem, \(a\) is a root of \(p\) if and only if \(X - a\) divides \(p\). For \(p \neq 0\), the multiplicity of \(a\) is the largest \(m\) such that \((X - a)^m\) divides \(p\); it is positive exactly when \(a\) is a root.

The roots of \(p\) are collected into a multiset, the multiset of roots of \(p\), in which each element \(a\) occurs as many times as its multiplicity as a root of \(p\). For nonzero \(p\), an element lies in this multiset exactly when it is a root of \(p\). Counting multiplicity, a nonzero polynomial has at most as many roots as its degree.

The bound comes from the factor theorem and the absence of zero divisors. If \(a\) is a root of a nonzero \(p\), then \(p = (X - a)\,q\) with \(\deg q = \deg p - 1\). Any root \(b \neq a\) of \(p\) satisfies \((b - a)\,q(b) = 0\), so \(q(b) = 0\), and the multiplicity of \(a\) in \(p\) is one more than in \(q\). A polynomial with no root has the empty multiset of roots, which starts an induction on the degree that finishes the argument.

Examples
Properties

The coefficients of a polynomial that splits are, up to sign and the leading coefficient, the elementary symmetric functions of its roots (Vieta's formulas). A nonconstant polynomial without roots in its coefficient field acquires them in a larger field: a rupture field of one of its irreducible factors contains at least one, and in a splitting field it splits completely. A nonzero polynomial over a field is separable exactly when it has no repeated roots in such a field. For real polynomials, Descartes' rule of signs bounds the number of positive roots. For nonconstant complex polynomials, the Gauss–Lucas theorem places the roots of the derivative in the convex hull of the roots.

In Mathlib

Mathlib defines the roots for polynomials over any commutative ring that is an integral domain, as a multiset, so that multiplicities are part of the data. The zero polynomial, at which every element vanishes, is assigned the empty multiset by convention; for this reason membership in the multiset is equivalent to being a root only for nonzero polynomials. Because Mathlib also gives the zero polynomial degree \(0\) in its natural-number version of the degree, the number of roots is at most that degree for every polynomial, with no nonzero hypothesis, and the statement about algebraically closed fields likewise holds for every polynomial. The roots of a polynomial in an algebra \(S\) over its coefficient ring, where \(S\) is an integral domain (for instance a larger field), are obtained by mapping its coefficients into \(S\) and taking the roots of the image; the set of distinct roots in \(S\) forgets multiplicities. Mathlib's notion of splitting is defined over the coefficient ring itself, as a product of constants and monic linear factors.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.roots
Uses 5 · Used by 10
Statement usesPolynomial in one indeterminate · Polynomial functions · Multiset · Multiplicity
Proof usesThe Factor and Remainder Theorems
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · Descartes Rule of Signs · Algebraically closed field · Splitting field · Separable polynomial · Schwartz–Zippel theorem · Gauss–Lucas theorem · Primitive complex roots of unity · Cyclotomic polynomials in \(\Q[X]\) · Relationship between the coefficients and the roots of a split polynomial

DefinitionMultiplicity#

The multiplicity of a root \(a\) of a polynomial \(p\) is the number of times the linear factor \(X - a\) occurs in \(p\): the largest \(m\) such that \((X - a)^m\) divides \(p\). It refines the yes-or-no question "is \(a\) a root?" into a count, distinguishing simple roots from double and higher roots. Counting roots with multiplicity is what makes statements such as "a polynomial of degree \(n\) over the complex numbers has exactly \(n\) roots" true, and multiplicity is closely tied to the derivative of a polynomial and to separability.

Definition

Let \(R\) be a commutative ring, \(p\) a nonzero polynomial with coefficients in \(R\), and \(a\) an element of \(R\). The multiplicity of \(a\) as a root of \(p\) is the largest natural number \(m\) such that \((X - a)^m\) divides \(p\). Such a largest \(m\) exists because \(X - a\) is monic, so a power of it that divides \(p\) cannot have degree larger than that of \(p\). Equivalently, for a nonzero \(p\) and every \(n\), \((X - a)^n\) divides \(p\) exactly when \(n\) is at most the multiplicity. In particular, if \(m\) is the multiplicity of \(a\) in a nonzero \(p\), then \(p = (X - a)^m q\) for a polynomial \(q\) not divisible by \(X - a\). By the factor theorem, \(X - a\) divides \(q\) exactly when \(q(a) = 0\), so the condition on \(q\) says \(q(a) \neq 0\).

For a nonzero \(p\), the multiplicity of \(a\) is positive exactly when \(a\) is a root of \(p\), so elements that are not roots have multiplicity \(0\). A root of multiplicity \(1\) is called simple, and a root of multiplicity at least \(2\) is called a multiple (double, triple, ...) root. The zero polynomial is divisible by every power of \(X - a\); by convention its multiplicity at every point is \(0\).

Examples
Properties

The characteristic-zero hypothesis in the formula for the multiplicity of a root of \(p'\) cannot be dropped. Over a field of prime characteristic \(\ell\), the polynomial \((X - a)^\ell\) has a root of multiplicity \(\ell\) at \(a\), but its derivative \(\ell\,(X - a)^{\ell-1}\) is the zero polynomial, whose multiplicity at \(a\) is \(0\) by convention rather than \(\ell - 1\).

Multiplicity of a root is the special case of the multiplicity of a prime factor in a unique factorisation domain: over a field \(K\), the polynomial ring \(K[X]\) is such a domain and \(X - a\) is one of its prime elements. The same idea gives the order of vanishing of an analytic function at a point, the valuation of an integer at a prime, and the intersection multiplicities of algebraic geometry.

In Mathlib

Mathlib defines the multiplicity for polynomials over an arbitrary ring, commutative or not, as a natural number, and it assigns the value \(0\) to the zero polynomial instead of infinity. With that convention, the multiplicity is \(0\) for the zero polynomial and, for a nonzero polynomial, agrees with Mathlib's general multiplicity of \(X - a\) as a divisor of \(p\). Many of the statements above therefore carry a hypothesis that some polynomial is nonzero, and additivity over products is proved for integral domains. The derivative test in characteristic zero is a corollary of a sharper statement: over any commutative ring, if \(a\) is a root of a nonzero polynomial \(p\) whose multiplicity \(m\), viewed as an element of the ring, is not a zero divisor, then the multiplicity of \(a\) as a root of \(p'\) is \(m - 1\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.rootMultiplicity
Uses 6 · Used by 1
Statement usesPolynomial in one indeterminate · Ring · Polynomial functions · The Factor and Remainder Theorems
Proof usesPolynomial derivative · Characteristic zero
Used byRoots of a polynomial

DefinitionSeparable polynomial#

A separable polynomial over a field is a nonzero polynomial without repeated roots: in any field over which it factors into linear factors, its roots are pairwise distinct. Separability can be decided inside the base field, without finding a single root, by checking that the polynomial and its formal derivative have no common factor of positive degree. The notion is basic to field theory: separable extensions, built from roots of separable polynomials, are the setting of the primitive element theorem and of Galois theory. In characteristic zero every irreducible polynomial is separable, so the subtleties live in characteristic \(p\).

Definition

Let \(R\) be a commutative ring, \(f \in R[X]\), and \(f'\) its formal derivative. The polynomial \(f\) is separable when \(f\) and \(f'\) are coprime in the sense of Bézout: \(f\) is separable exactly when there are polynomials \(a, b \in R[X]\) with \(af + bf' = 1\).

Over a field \(F\) the ring \(F[X]\) is a Euclidean domain, so the condition says that \(f\) and \(f'\) have no common factor of positive degree, which the Euclidean algorithm decides. The connection with roots is the following: if a nonzero polynomial \(f\) over \(F\) splits into linear factors over an extension field \(K\), then \(f\) is separable if and only if its roots in \(K\) are pairwise distinct, that is, each root has multiplicity one. Taking \(K\) to be a splitting field of \(f\) gives the definition by roots. The reason is the product rule: if \((X - \alpha)^2\) divides \(f\), then \(X - \alpha\) divides \(f'\); conversely, if \(f = (X - \alpha)g\) and \(f'(\alpha) = 0\), then \(g(\alpha) = 0\), so \(\alpha\) is a repeated root. Since \(f\) splits over \(K\), any common factor of positive degree of \(f\) and \(f'\) has a root in \(K\), which is then a common root of \(f\) and \(f'\).

For an irreducible polynomial the test is simpler, since the only candidate for a common factor of \(f\) and \(f'\) is \(f\) itself, up to a nonzero constant factor, which can divide \(f'\) only if \(f' = 0\), because \(f'\) has smaller degree than \(f\): an irreducible polynomial \(f\) over a field is separable if and only if \(f' \neq 0\).

Examples
Properties
In Mathlib

Mathlib defines separability for polynomials over any commutative semiring, directly as Bézout coprimality of the polynomial and its formal derivative; roots play no part in the definition, and the description by distinct roots over a field is a theorem. The definition fixes the edge cases: the zero polynomial is not separable over a nonzero ring, nonzero constants over a field are separable because they are units, and over the zero ring every polynomial is separable. It is the strict notion, under which a polynomial with a repeated irreducible factor, such as \((X - 1)^2\), is not separable; some texts instead call a polynomial separable when each of its irreducible factors has distinct roots, and under that convention \((X - 1)^2\) would count as separable. Separable elements are defined for algebras over a commutative ring through the minimal polynomial. Since Mathlib gives a non-integral element the minimal polynomial \(0\), a separable element is automatically integral, and separable extensions are algebraic.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.Separable
Uses 4 · Used by 4
Statement usesPolynomial in one indeterminate · Polynomial derivative · Coprime element · Roots of a polynomial
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Dirichlet’s Theorem · Primitive element theorem · Jordan-Chevalley-Dunford decomposition

Instance\(K[X]\) is Euclidean#

For a field \(K\), the ring \(K[X]\) of polynomials in one indeterminate over \(K\) is a Euclidean domain: any polynomial can be divided by a nonzero polynomial, leaving a remainder of smaller degree. This fact, \(K[X]\) is Euclidean, makes the arithmetic of polynomials over a field closely parallel to the arithmetic of the integers. It yields a Euclidean algorithm for greatest common divisors, shows that every ideal of \(K[X]\) is principal and that polynomials factor uniquely into irreducibles, and underlies the construction of field extensions by adjoining roots.

Statement

Let \(K\) be a field. The polynomial ring \(K[X]\) is a Euclidean domain, with the degree as its size function. Concretely, for polynomials \(f\) and \(g\) with \(g \neq 0\) there are polynomials \(q\) (the quotient) and \(r\) (the remainder) with

\[f = g\,q + r, \qquad \deg r < \deg g,\]

where the zero polynomial is taken to have degree smaller than every natural number. The pair \((q, r)\) is unique, as shown in the Proof section. In Mathlib's notation the existence part consists of the identity \(f = g\,(f / g) + f \bmod g\), valid in every Euclidean domain, and the bound \(\deg (f \bmod g) < \deg g\) for \(g \neq 0\).

Examples
  • Over the rationals, dividing \(X^3 + 2X + 1\) by \(X^2 + 1\) gives \(X^3 + 2X + 1 = (X^2 + 1)\,X + (X + 1)\), with remainder of degree \(1 < 2\).
  • Dividing by a linear polynomial \(X - a\) leaves a constant remainder, and that constant is the value of the polynomial at \(a\): the remainder of \(f\) on division by \(X - a\) is \(f(a)\). Hence \(X - a\) divides \(f\) if and only if \(a\) is a root of \(f\), the content of the factor and remainder theorems.
  • The Euclidean algorithm applied to \(X^2 - 1\) and \(X^2 - 3X + 2\) over the rationals runs \(X^2 - 1 = (X^2 - 3X + 2) \cdot 1 + (3X - 3)\) and then \(X^2 - 3X + 2 = (3X - 3)\,\tfrac{1}{3}(X - 2)\), so the last nonzero remainder \(3X - 3\) is a greatest common divisor; its monic multiple is \(X - 1\).
  • The hypothesis that \(K\) is a field cannot be dropped. In \(\mathbb{Z}[X]\), dividing \(X\) by \(2\) would need a remainder of degree less than \(\deg 2 = 0\), that is, a remainder of zero and \(X = 2q\), which is impossible. More decisively, the ideal generated by \(2\) and \(X\) is not principal, so \(\mathbb{Z}[X]\) is not Euclidean for any choice of size function.
Consequences
Proof

Fix \(g \neq 0\) of degree \(m\) with leading coefficient \(c\). If \(\deg f < m\), take \(q = 0\) and \(r = f\). Otherwise let \(f\) have degree \(n \ge m\) and leading coefficient \(a\). Since \(K\) is a field, \(c\) is invertible, and \(f - a c^{-1} X^{n-m} g\) has degree less than \(n\). By induction on the degree it can be written as \(g q' + r\) with \(\deg r < m\), so \(f = g\,(q' + a c^{-1} X^{n-m}) + r\). For uniqueness, if \(g q + r = g q' + r'\) then \(g\,(q - q') = r' - r\); the right side has degree less than \(m\). If \(h = q - q'\) were nonzero, then \(c\) times the leading coefficient of \(h\) would be nonzero, because \(c\) is invertible, and when the product of the leading coefficients is nonzero, the degree of a product is the sum of the degrees, so \(g h\) would have degree at least \(m\). Hence \(q = q'\) and \(r = r'\). Finally, \(K[X]\) is an integral domain, as a Euclidean domain must be: over a field the degree of a product is the sum of the degrees, so a product of nonzero polynomials is nonzero.

In the division argument the only use of the field hypothesis is to invert the leading coefficient of \(g\). Over any commutative ring the same argument divides by a polynomial whose leading coefficient is \(1\), and for such a monic divisor the quotient and remainder are again unique.

The integers are the other basic Euclidean domain, with the absolute value as size function (\(\mathbb{Z}\) is a Euclidean ring). For an integral domain \(R\) the property singles out fields: if \(R[X]\) is a principal ideal domain, then \(R\) is a field, so \(R[X]\) is Euclidean only when \(R\) is a field. Rings such as \(\mathbb{Z}[X]\) and the polynomial rings in two or more indeterminates over a field are not principal ideal domains, but they keep unique factorization (\(A[{X_i}]\) is a UFD when \(A\) is a UFD).

In Mathlib

Mathlib defines a Euclidean domain as a nontrivial commutative ring with quotient and remainder operations satisfying \(b\,(a/b) + a \bmod b = a\), together with a well-founded relation under which the remainder on division by a nonzero element lies below the divisor and no product \(ab\) with \(b \neq 0\) lies below \(a\). This relation takes the place of a size function to the natural numbers. For polynomials over a field this relation compares degrees, and Mathlib's degree takes the value \(-\infty\) on the zero polynomial, which places \(0\) below every other polynomial. By convention division by the zero polynomial gives quotient \(0\) and leaves the dividend as remainder. The greatest common divisor computed by the Euclidean algorithm is one greatest common divisor, not necessarily monic; Mathlib also equips \(K[X]\) with a normalized greatest common divisor, which is monic unless both polynomials are zero (compare \(A[X]\) has gcd and lcm if \(A\) does).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.instEuclideanDomain
Uses 3 · Used by 5
Statement usesField · Polynomial in one indeterminate · Euclidean domain
Used by\(A[{X_i}]\) is a UFD when \(A\) is a UFD · Eisenstein's criterion · Mason–Stothers theorem · Primitive element theorem · Ostrowski's theorem

TheoremHilbert basis theorem#

The Hilbert basis theorem says that if \(R\) is a commutative Noetherian ring, then so is the polynomial ring \(R[x]\). Applied repeatedly, it shows that every ideal of a polynomial ring in finitely many variables over a field, or over the integers, is generated by finitely many polynomials. It is one of the basic finiteness results of commutative algebra and algebraic geometry: it guarantees that any system of polynomial equations, however large, has the same solutions as some finite subsystem.

Statement

Let \(R\) be a commutative Noetherian ring, so that every ideal of \(R\) is finitely generated. Then \(R[x]\) is Noetherian as well: for each ideal \(I\) of \(R[x]\) there are polynomials \(f_1, \dots, f_m \in I\) such that every element of \(I\) has the form

\[g_1 f_1 + \cdots + g_m f_m, \qquad g_1, \dots, g_m \in R[x].\]

By induction on the number of variables, the polynomial ring \(R[x_1, \dots, x_n]\) in finitely many variables is Noetherian (see polynomial in several indeterminates), since \(R[x_1, \dots, x_n]\) is the polynomial ring in one variable \(x_n\) over \(R[x_1, \dots, x_{n-1}]\).

Examples
  • Taking \(R\) to be a field \(k\), every ideal of \(k[x_1, \dots, x_n]\) is finitely generated. For \(n = 1\) this is already clear, because \(k[x]\) is a principal ideal domain; for \(n \ge 2\) the ring \(k[x_1, \dots, x_n]\) is not a principal ideal domain (the ideal \((x_1, x_2)\) is not principal), and the theorem gives finite generation, though no bound on the number of generators.
  • Taking \(R\) to be the integers, the rings \(\mathbb{Z}[x]\) and \(\mathbb{Z}[x, y]\) are Noetherian. Neither is a principal ideal domain: in both rings the ideal \((2, x)\) is not principal.
  • The ring of Gaussian integers \(\mathbb{Z}[i]\) is isomorphic to \(\mathbb{Z}[x]/(x^2 + 1)\), and a quotient of a commutative Noetherian ring by an ideal is Noetherian (see quotient ring), so \(\mathbb{Z}[i]\) is Noetherian.
  • The hypothesis of finitely many variables cannot be dropped: in \(k[x_1, x_2, x_3, \dots]\) the chain \((x_1) \subsetneq (x_1, x_2) \subsetneq (x_1, x_2, x_3) \subsetneq \cdots\) never stops, so the ideal generated by all the variables is not finitely generated.
Consequences
Proof

Let \(I\) be an ideal of \(R[x]\). For each \(n \ge 0\) let \(L_n\) be the set of leading coefficients of the polynomials in \(I\) of degree at most \(n\), the zero polynomial contributing \(0\). Equivalently, \(L_n\) is the set of coefficients of \(x^n\) in the polynomials of \(I\) of degree at most \(n\), a description under which it is visibly closed under addition and under multiplication by elements of \(R\); so \(L_n\) is an ideal of \(R\). Moreover multiplying a polynomial by a power of \(x\) does not change its leading coefficient, so \(L_m \subseteq L_n\) whenever \(m \le n\). Because \(R\) is Noetherian, this increasing chain stops: there is an \(N\) with \(L_n = L_N\) for all \(n \ge N\).

The polynomials of degree at most \(N\) form a finitely generated \(R\)-module, so the submodule of those lying in \(I\) is finitely generated too, \(R\) being Noetherian: \(I\) contains finitely many polynomials of degree at most \(N\) that span, over \(R\), all the polynomials in \(I\) of degree at most \(N\). Let \(J\) be the ideal of \(R[x]\) that they generate; then \(J \subseteq I\).

Every \(p \in I\) lies in \(J\). The case \(p = 0\) is clear; otherwise argue by induction on the degree \(k\) of \(p\). If \(k \le N\), this holds by the choice of the generators. If \(k > N\), the leading coefficient of \(p\) lies in \(L_k = L_N\), so it is the leading coefficient of some \(q \in I\) of degree \(d \le N\), and \(q \in J\). The polynomial \(p - x^{k-d} q\) lies in \(I\) and is either zero or of degree less than \(k\), so it lies in \(J\) by induction, and therefore so does \(p\). Hence \(I = J\) is finitely generated.

Generalizations

The theorem holds without commutativity: if every left ideal of a ring \(R\) is finitely generated, the same is true of \(R[x]\), by the same argument. The several-variable form above holds for any finite set of variables, and the analogue for power series is listed among the consequences.

In Mathlib

Mathlib states the theorem for commutative rings. A ring is Noetherian in Mathlib when it is a Noetherian module over itself, which amounts to every ideal being finitely generated. The theorem is registered so that the Noetherian property of a polynomial ring is found automatically from that of its coefficient ring. The several-variable version allows the variables to be indexed by any finite type rather than by the numbers \(1, \dots, n\). Instead of an increasing chain of ideals that stabilizes, the formal proof uses an equivalent form of the Noetherian condition: among the ideals \(L_n\) it picks one that is maximal, which then contains all the others.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.isNoetherianRing
Uses 5
Statement usesNoetherian ring · Polynomial in one indeterminate · Ideal of a commutative ring
Proof usesNoetherian module · Generating sets

Instance\(A[X]\) has gcd and lcm if \(A\) does#

The statement that \(A[X]\) has gcd and lcm if \(A\) does says that if every two elements of an integral domain \(A\) have a greatest common divisor and a least common multiple, then the same holds in the polynomial ring \(A[X]\). In other words, the polynomial ring over a GCD domain is again a GCD domain. The result explains why polynomials over the integers, or over any unique factorisation domain, admit gcds even though division with remainder is not available in general, and it is the main structural output of the theory of contents and primitive polynomials around Gauss's lemma.

Statement

Let \(A\) be an integral domain. An element \(d\) is a greatest common divisor of \(a\) and \(b\) if \(d\) divides both and every common divisor of \(a\) and \(b\) divides \(d\); equivalently, an element divides \(\gcd(a,b)\) exactly when it divides both \(a\) and \(b\). Dually, \(\operatorname{lcm}(a,b)\) divides an element exactly when \(a\) and \(b\) both divide it. These are determined only up to multiplication by a unit, so one fixes a normalization: a rule choosing one representative in each class of associated elements, such as the nonnegative integer in \(\mathbb{Z}\).

Theorem. If \(A\) is an integral domain equipped with a normalization in which every pair of elements has a normalized gcd and lcm, then \(A[X]\) carries the same structure. The normalization on \(A[X]\) is induced from \(A\): a polynomial \(p\) is normalized by multiplying it by the constant unit that normalizes its leading coefficient, so a polynomial counts as normalized exactly when its leading coefficient is normalized in \(A\). In particular, the leading coefficient of the normalization of \(p\) is the normalization of the leading coefficient of \(p\).

When \(A\) is a field, every nonzero element normalizes to \(1\), so the gcd of two polynomials, not both zero, is the monic gcd familiar from the Euclidean algorithm in \(A[X]\).

Examples
  • Integer polynomials. In \(\mathbb{Z}[X]\) take \(p = 6X^2 - 6 = 6(X-1)(X+1)\) and \(q = 4X^2 + 8X + 4 = 4(X+1)^2\). The contents (gcds of the coefficients) are \(6\) and \(4\), with gcd \(2\), and the primitive parts \((X-1)(X+1)\) and \((X+1)^2\) have gcd \(X+1\), so \(\gcd(p,q) = 2X + 2\); similarly \(\operatorname{lcm}(p,q) = 12(X-1)(X+1)^2\). The product of the gcd and the lcm is \(24(X-1)(X+1)^3 = pq\).
  • Gcds without Bézout. In \(\mathbb{Z}[X]\) the gcd of \(2\) and \(X\) is \(1\), yet \(1\) is not of the form \(2f + Xg\), since every such polynomial has an even constant term. So Bézout's identity fails, so gcds in \(A[X]\) cannot be produced by a Euclidean algorithm that tracks Bézout coefficients.
  • Beyond unique factorisation. Every unique factorisation domain with a chosen normalization is a GCD domain, but not conversely: the ring of all algebraic integers is a GCD domain with no irreducible elements at all. The theorem applies to such rings as well.
Content and primitive polynomials

Over a GCD domain \(A\), the content of a polynomial \(p\) is the gcd of its coefficients. A polynomial is primitive when the only constants dividing it are units, which over a GCD domain means that its content is \(1\). Every polynomial factors as its content times a primitive part, and the primitive part is primitive. The key facts are the forms of Gauss's lemma:

From these one obtains a divisibility test: for \(q \neq 0\), \(p\) divides \(q\) if and only if the content of \(p\) divides that of \(q\) and the primitive part of \(p\) divides that of \(q\).

Proof

It suffices to construct least common multiples; in a cancellative commutative monoid with zero in which every pair has an lcm, the gcd of two nonzero elements is their product divided by their lcm.

First, any two primitive polynomials \(p\) and \(q\) have a primitive lcm. Among the primitive common multiples of \(p\) and \(q\) (the product \(pq\) is one), choose \(r\) of least degree. Let \(s\) be any nonzero common multiple; replacing \(s\) by its primitive part, one may assume \(s\) primitive, so \(\deg r \le \deg s\). If \(s\) is constant, then so is \(r\), and a primitive constant is a unit. Otherwise the polynomial

\[s' = \operatorname{lc}(r)\, s - \operatorname{lc}(s)\, X^{\deg s - \deg r}\, r\]

is a common multiple of smaller degree, where \(\operatorname{lc}\) denotes the leading coefficient. By induction on degree \(r\) divides \(s'\), hence divides \(\operatorname{lc}(r)\,s\), and because \(r\) is primitive Gauss's lemma lets one cancel the constant: \(r\) divides \(s\).

For arbitrary \(p\) and \(q\), let \(r\) be a primitive lcm of their primitive parts. Then \(\operatorname{lcm}(c(p), c(q))\, r\), with \(c\) the content, is an lcm of \(p\) and \(q\): by the divisibility test, a nonzero \(s\) is a multiple of both exactly when \(c(s)\) is a multiple of \(c(p)\) and \(c(q)\) and the primitive part of \(s\) is a multiple of both primitive parts.

Consequences
  • By induction on the number of variables, \(A[X_1, \dots, X_n]\) is a GCD domain whenever \(A\) is; for instance \(\mathbb{Z}[X,Y]\) and \(K[X,Y]\) over a field \(K\).
  • For \(p \neq 0\), the gcd of \(p\) and \(q\) has degree at most that of \(p\).
  • The parallel statement for factorisation, that a polynomial ring over a unique factorisation domain is again one, is the companion theorem on polynomial rings over UFDs; its conclusion is stronger, but the gcd version also covers GCD domains that are not UFDs.
In Mathlib

Mathlib records the theorem as an instance: a commutative ring with a normalized gcd structure yields one on its polynomial ring. A gcd structure includes cancellation of nonzero factors, so the base ring is automatically an integral domain or the zero ring; nontriviality is never assumed. Gcd and lcm are total operations, normalized so that they are well defined rather than defined up to units; the gcd of \(0\) and \(0\) is \(0\). The proof constructs the lcm as above, choosing it from an existence statement, and derives the gcd from it; the resulting operations are noncomputable. Separate instances transfer the version with a multiplicative normalization, and the bare property of having gcds without a chosen normalization, to the polynomial ring. The common textbook route through the field of fractions is not used.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.normalizedGcdMonoid
Uses 3
Statement usesGreatest common divisor · Least common multiple · Polynomial in one indeterminate

Theorem\(A[{X_i}]\) is a UFD when \(A\) is a UFD#

Polynomial rings over a unique factorisation domain are unique factorisation domains: if \(A\) is a unique factorisation domain (UFD), then so is the polynomial ring \(A[X_i : i \in I]\) in any family of indeterminates, finite or infinite. Together with the fact that every field and the ring of integers are UFDs, it shows that the rings \(k[X_1, \dots, X_n]\) and \(\mathbb{Z}[X_1, \dots, X_n]\) have unique factorisation, although most of them are not principal ideal domains.

Statement

Let \(A\) be a UFD and \(I\) any set. Then the polynomial ring \(A[X_i : i \in I]\) is a UFD: it is an integral domain, every nonzero polynomial that is not a unit is a product of irreducible polynomials, and two such factorisations of the same polynomial have the same factors up to order and multiplication by units. The case of one variable reads: if \(A\) is a UFD, then so is \(A[X]\).

The converse also holds: if \(A[X_i : i \in I]\) is a UFD, then so is \(A\) (trivially so when \(I\) is empty). Degrees add under multiplication over a domain, so a factorisation of a constant polynomial involves only constants, and unique factorisation in \(A[X_i]\) restricts to unique factorisation in \(A\).

Examples
  • Integer polynomials. \(\mathbb{Z}[X]\) is a UFD but not a principal ideal domain: the ideal generated by \(2\) and \(X\) is not principal.
  • Several variables over a field. For a field \(k\) and \(n \ge 2\), the ring \(k[X_1, \dots, X_n]\) is a UFD but not a principal ideal domain: the ideal generated by \(X_1\) and \(X_2\) is not principal. In \(\mathbb{Q}[X, Y]\), for instance, \(X^2Y - Y^3 = Y(X - Y)(X + Y)\) is the factorisation into irreducibles, unique up to the order of the factors and nonzero rational constants.
  • The variables themselves. Over any integral domain, each variable \(X_i\) is a prime element of the polynomial ring, that is, a nonzero nonunit \(p\) such that whenever \(p\) divides a product \(ab\), it divides \(a\) or \(b\).
  • Infinitely many variables. \(k[X_1, X_2, X_3, \dots]\) is a UFD that is not Noetherian: the ideals \((X_1) \subset (X_1, X_2) \subset \cdots\) form a strictly increasing chain. The Hilbert basis theorem gives Noetherianity only for finitely many variables over a Noetherian ring; this example shows that unique factorisation does not need it.
  • A failure. \(\mathbb{Z}[\sqrt{-5}]\) is not a UFD, since \(6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5})\), where \(2\), \(3\) and \(1 \pm \sqrt{-5}\) are irreducible (the norm \(N(a + b\sqrt{-5}) = a^2 + 5b^2\) takes the values \(4\), \(9\) and \(6\) on them and never the values \(2\) or \(3\)) and \(2\) is not associate to \(1 \pm \sqrt{-5}\); by the converse above neither is \(\mathbb{Z}[\sqrt{-5}][X]\).
Proof

One variable. Let \(K\) be the field of fractions of \(A\). Call a polynomial in \(A[X]\) primitive when its coefficients have no common divisor other than units. Every nonzero \(f\) can be written as \(f = c f_0\) with \(c \in A\) (a greatest common divisor of the coefficients) and \(f_0\) primitive. Gauss's lemma has three parts, all valid over a UFD: the product of two primitive polynomials is primitive (Mathlib assumes a normalised gcd function on \(A\), which every UFD can be given); a primitive polynomial is irreducible in \(A[X]\) if and only if it is irreducible in \(K[X]\); and a primitive polynomial that divides another in \(K[X]\) already divides it in \(A[X]\).

For existence, factor \(c\) in \(A\), and factor \(f_0\) in \(K[X]\), a UFD because \(K[X]\) is a Euclidean domain; clearing denominators turns each factor into a primitive polynomial of \(A[X]\), irreducible by the second part of the lemma, and their product is primitive by the first part. It equals \(f_0\) up to a nonzero factor in \(K\); since both are primitive, comparing contents shows that this factor is a unit of \(A\). For uniqueness it suffices to show that every irreducible element is prime. An irreducible constant is a prime of \(A\) and stays prime in \(A[X]\). An irreducible nonconstant polynomial is primitive and irreducible in \(K[X]\), hence prime there, and the third part of the lemma brings divisibility back from \(K[X]\) to \(A[X]\). Finally, a domain is a UFD exactly when every nonzero element is a unit times a product of primes.

Finitely many variables. By induction on \(n\), using that the ring in \(n + 1\) variables is isomorphic to the polynomials in one variable over the ring in \(n\) variables, and that a ring isomorphic to a UFD is a UFD.

Arbitrary variables. Every polynomial is the image of a polynomial in finitely many of the variables, and for a subset \(S\) of \(I\), a polynomial in the variables indexed by \(S\) is prime in \(A[X_i : i \in S]\) if and only if it is prime in \(A[X_i : i \in I]\). So a factorisation into primes in a finite polynomial ring stays a factorisation into primes in the large one, and the criterion above applies.

In Mathlib

Mathlib registers the result as an instance, so the polynomial ring over a UFD is recognised as one automatically. The indeterminates are indexed by an arbitrary type, with no finiteness assumption, and the proof for many variables follows the reduction above: finitely many variables by induction, then the general case because each polynomial involves only finitely many of the variables. Mathlib's notion of unique factorisation requires cancellation of nonzero factors but not \(0 \neq 1\), so the zero ring qualifies and the theorem holds for it trivially. For one variable Mathlib takes a different route from the textbook proof: it shows that strict divisibility in \(A[X]\) is well-founded (there is no infinite chain of proper divisors), comparing degrees and then leading coefficients, and that \(A[X]\) has greatest common divisors; in a domain with greatest common divisors every irreducible element is prime, and these two facts together give unique factorisation.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMvPolynomial.uniqueFactorizationMonoid
Uses 7
Statement usesUnique factorisation domain · Polynomial in several indeterminates · Polynomial in one indeterminate · Irreducible element
Proof usesField of fractions of an integral domain · Greatest common divisor · \(K[X]\) is Euclidean

TheoremEisenstein's criterion#

Eisenstein's criterion is a sufficient condition for a polynomial to be irreducible, read off from its coefficients alone. In its best-known form it says that an integer polynomial whose leading coefficient is not divisible by a prime \(p\), whose other coefficients are all divisible by \(p\), and whose constant term is not divisible by \(p^2\), cannot be factored into polynomials of lower degree with rational coefficients. Irreducibility is hard to decide in general, and the criterion produces irreducible polynomials of every degree with almost no work; it is the standard tool for showing that cyclotomic polynomials of prime index and polynomials such as \(x^n - 2\) are irreducible.

Statement

Let \(R\) be an integral domain, let \(P\) be a prime ideal of \(R\), and let

\[f = a_n x^n + a_{n-1} x^{n-1} + \cdots + a_1 x + a_0 \in R[x]\]

have degree \(n \ge 1\). Suppose that \(f\) is primitive, meaning that the only constant polynomials dividing \(f\) are units of \(R\). If

  • the leading coefficient \(a_n\) does not lie in \(P\),
  • the coefficients \(a_0, a_1, \dots, a_{n-1}\) all lie in \(P\), and
  • the constant term \(a_0\) does not lie in \(P^2\),

then \(f\) is irreducible in \(R[x]\). A polynomial satisfying the three coefficient conditions is said to be Eisenstein at \(P\).

For \(R = \mathbb{Z}\) and \(P = (p)\) with \(p\) a prime number, the conditions read \(p \nmid a_n\), \(p \mid a_i\) for \(i < n\), and \(p^2 \nmid a_0\). Primitivity is automatic for a monic polynomial, and in general it is needed only for irreducibility in \(R[x]\) itself: when \(R\) is a GCD domain such as \(\mathbb{Z}\), it can be dropped for irreducibility over the field of fractions (see below). Over an arbitrary integral domain the coefficient conditions do not guarantee irreducibility over the field of fractions: in \(k[t^2, t^3][x]\), with \(k\) a field, the monic polynomial \(x^2 - t^2\) is Eisenstein at the prime ideal \((t^2, t^3)\), because \(t^2\) does not lie in \((t^2, t^3)^2 = (t^4, t^5, t^6)\), yet over \(k(t)\) it equals \((x - t)(x + t)\).

Examples
  • Pure powers. For a prime \(p\) and \(n \ge 1\), the polynomial \(x^n - p\) is monic and Eisenstein at \(p\), so it is irreducible over \(\mathbb{Z}\), and hence over \(\mathbb{Q}\). In particular \(\mathbb{Q}[x]\) has irreducible polynomials of every degree.
  • Cyclotomic polynomials of prime index. For a prime \(p\), the cyclotomic polynomial \(\Phi_p(x) = x^{p-1} + \cdots + x + 1\) is not itself Eisenstein, but after the substitution \(x \mapsto x + 1\), $\(\Phi_p(x+1) = \frac{(x+1)^p - 1}{x} = \sum_{k=1}^{p} \binom{p}{k} x^{k-1}.\)$ Its leading coefficient is \(1\), the binomial coefficients \(\binom{p}{k}\) with \(1 \le k \le p-1\) are divisible by \(p\), and the constant term is \(p\), so \(\Phi_p(x+1)\) is Eisenstein at \(p\). Substitution of \(x + 1\) for \(x\) is a ring automorphism of \(\mathbb{Z}[x]\), so \(\Phi_p\) is irreducible.
  • Shifting. The same device handles \(x^2 + 1\), which is Eisenstein at no prime: replacing \(x\) by \(x + 1\) gives \(x^2 + 2x + 2\), which is Eisenstein at \(2\).
  • Polynomials over other rings. If \(k\) is a field, the ideal \((t)\) of \(k[t]\) is prime, and \(x^n - t\) is Eisenstein at \((t)\); so \(x^n - t\) is irreducible in \(k[t][x]\) for every \(n \ge 1\).

The hypotheses cannot be dropped. The polynomial \(x^2 - 4 = (x-2)(x+2)\) satisfies every condition at \(p = 2\) except that its constant term lies in \((2)^2 = (4)\). The polynomial \(2x + 6 = 2(x + 3)\) is Eisenstein at \(3\) but not primitive, and it is reducible in \(\mathbb{Z}[x]\) because \(2\) is not a unit there, although it is irreducible in \(\mathbb{Q}[x]\). The criterion is only sufficient: \(x^2 + x + 1\) has no rational root, so it is irreducible over \(\mathbb{Q}\), but it is Eisenstein at no prime, since no prime divides its middle coefficient \(1\).

Proof

Since \(R\) is an integral domain, the units of \(R[x]\) are constants, so \(f\), of positive degree, is not a unit. Suppose \(f = gh\) in \(R[x]\). If \(g\) is a constant \(c\), then \(c\) divides \(f\), so \(c\) is a unit by primitivity; likewise for \(h\). It remains to rule out a factorization in which \(g\) and \(h\) both have positive degree. Since \(a_n\) is the product of the leading coefficients of \(g\) and \(h\) and \(a_n \notin P\), neither leading coefficient lies in \(P\).

Reduce coefficients modulo \(P\). The quotient ring \(R/P\) is an integral domain; let \(F\) be its field of fractions. In \(F[x]\) the reduction of \(f\) is \(\bar a_n x^n\) with \(\bar a_n \neq 0\), so \(\bar g \bar h = \bar a_n x^n\). Polynomials over a field form a Euclidean domain and so factor uniquely, and \(x\) is irreducible, so \(\bar g = u x^k\) and \(\bar h = v x^m\) for nonzero constants \(u, v \in F\). The leading coefficients of \(g\) and \(h\) survive reduction, so \(k = \deg g \ge 1\) and \(m = \deg h \ge 1\). Hence the constant terms \(g(0)\) and \(h(0)\) both reduce to \(0\), that is, both lie in \(P\), and \(a_0 = g(0)\,h(0) \in P^2\), a contradiction.

Consequences

Over a GCD domain \(R\) (an integral domain in which any two elements have a greatest common divisor; every unique factorisation domain, such as \(\mathbb{Z}\), is one) with field of fractions \(K\), a primitive polynomial is irreducible in \(R[x]\) exactly when it is irreducible in \(K[x]\) (Gauss's lemma). So a primitive polynomial of positive degree that is Eisenstein at a prime ideal of \(R\) is irreducible in \(K[x]\). Primitivity is not needed for this conclusion: writing \(f = c f_1\) with \(c \in R\) and \(f_1\) primitive, the element \(c\) is not in \(P\) because \(a_n \notin P\), so \(f_1\) is again Eisenstein at \(P\), hence irreducible in \(K[x]\), and \(f\) differs from it by a nonzero constant. For \(R = \mathbb{Z}\) this is the classical form: an integer polynomial of positive degree that is Eisenstein at some prime \(p\) is irreducible over \(\mathbb{Q}\).

Eisenstein's criterion is one of several coefficient tests for irreducibility; the rational root theorem reduces the search for a linear factor over \(\mathbb{Q}\) to finitely many candidates, which settles irreducibility over \(\mathbb{Q}\) in degrees \(2\) and \(3\). The shift used for \(\Phi_p\) also works for prime powers: for a prime \(p\) and \(k \ge 1\), \(\Phi_{p^k}(x+1)\) is Eisenstein at \(p\). Irreducibility of every cyclotomic polynomial needs a different argument: \(\Phi_n\) is irreducible over \(\mathbb{Z}\) for every \(n \ge 1\).

In Mathlib

Mathlib states the criterion for an arbitrary integral domain and an arbitrary prime ideal, and its conclusion is irreducibility in \(R[x]\) itself, which is why primitivity appears as a hypothesis; passing to the field of fractions is left to Gauss's lemma. The three coefficient conditions are also packaged as a predicate, being Eisenstein at an ideal, which does not include positive degree; a primitive polynomial of positive degree that is Eisenstein at a prime ideal is irreducible. The classical criterion is derived as a special case of a more general one: for an \(R\)-algebra \(K\) that is a field and a monic \(q \in R[x]\) whose image in \(K[x]\) is irreducible, a primitive \(f\) of positive degree is irreducible when its leading coefficient is nonzero in \(K\), its image in \(K[x]\) is that leading coefficient times a power of the image of \(q\), and the remainder of \(f\) on division by \(q\) is nonzero modulo \(P^2\), where \(P\) is the kernel of the map from \(R\) to \(K\). Taking \(K\) to be the field of fractions of \(R/P\) and \(q = x\) gives Eisenstein's criterion.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.irreducible_of_eisenstein_criterion
Uses 7 · Used by 1
Statement usesPolynomial in one indeterminate · Prime ideal · Irreducible element
Proof usesQuotient ring · Field of fractions of an integral domain · \(K[X]\) is Euclidean · Unique factorisation domain
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem)

AbbreviationPolynomial in several indeterminates#

A polynomial in several indeterminates over a commutative ring \(R\) is a finite sum of terms \(c\,X_1^{a_1}X_2^{a_2}\cdots X_n^{a_n}\) with coefficients \(c\) in \(R\), such as \(x^2 + y^2 - 1\) or \(xyz - 2\). These polynomials form a commutative ring, written \(R[X_1, \dots, X_n]\) or \(R[X_i : i \in I]\), which generalizes the polynomials in one indeterminate. It is a basic object of commutative algebra and algebraic geometry: every finitely generated commutative \(R\)-algebra is a quotient of such a ring, and the solution sets of systems of polynomial equations are studied through its ideals.

Definition

Let \(R\) be a commutative ring and \(I\) a set indexing the indeterminates; \(I\) may be infinite. An exponent vector is a function \(\alpha \colon I \to \mathbb{N}\) that is zero outside a finite set (a finitely supported function), and to each exponent vector corresponds a monomial

\[X^\alpha = \prod_{i \in I} X_i^{\alpha(i)},\]

a finite product since almost all exponents vanish. A polynomial is a formal finite sum \(p = \sum_\alpha p_\alpha X^\alpha\), that is, a function \(\alpha \mapsto p_\alpha\) from exponent vectors to \(R\) with only finitely many nonzero values. Polynomials are added coefficientwise, and multiplied by extending the rule \(X^\alpha \cdot X^\beta = X^{\alpha + \beta}\) bilinearly, so that

\[(pq)_\gamma = \sum_{\alpha + \beta = \gamma} p_\alpha\, q_\beta.\]

The result is the polynomial ring in the indeterminates \(X_i\) with coefficients in \(R\). By construction, two polynomials with the same coefficient at every monomial are equal, and every polynomial is the sum of its finitely many nonzero terms. Each term is a constant times a product of powers of indeterminates: \(c\,X^\alpha\) is the constant \(c\) times \(\prod_i X_i^{\alpha(i)}\). The map sending \(c\) to the constant polynomial \(c\) is injective, so \(R\) sits inside the polynomial ring.

The total degree of a nonzero polynomial is the largest value of \(\sum_i \alpha(i)\) over the exponent vectors \(\alpha\) with \(p_\alpha \neq 0\); for example \(x^3 y + y^2\) has total degree \(4\).

Examples
Properties

Universal property. For every commutative \(R\)-algebra \(A\) (see associative algebra) and every family \((a_i)_{i \in I}\) of elements of \(A\), there is an \(R\)-algebra homomorphism from \(R[X_i : i \in I]\) to \(A\) sending each \(X_i\) to \(a_i\), and it is the only \(R\)-algebra homomorphism that agrees with it on every \(X_i\). This homomorphism is evaluation, or substitution, at the point \((a_i)\). In this sense the polynomial ring is the free commutative \(R\)-algebra on the set \(I\); dropping commutativity gives the free algebra. Polynomials also admit induction: a statement that holds for constants, is preserved by sums, and is preserved by multiplication by an indeterminate holds for every polynomial.

Ring-theoretic properties.

Polynomials and functions. Each polynomial \(p\) over \(R\) defines a function \(R^I \to R\) by evaluation. If \(R\) is an infinite integral domain, two polynomials that agree at every point of \(R^I\) are equal, so polynomials may be identified with the functions they define. Over a finite field this fails: over a field with \(q\) elements, \(X_1^q - X_1\) is a nonzero polynomial that vanishes at every point.

Every polynomial is uniquely a sum of homogeneous polynomials, one in each total degree (see decomposition into homogeneous components). The Nullstellensatz describes, over an algebraically closed field, which polynomials in finitely many indeterminates vanish on the common zeros of an ideal, and the Schwartz–Zippel theorem bounds how many points of a finite grid a nonzero polynomial over an integral domain can vanish at. Allowing infinite sums of monomials in one indeterminate gives power series.

In Mathlib

Mathlib allows the coefficients to lie in any commutative semiring, so polynomials with natural-number coefficients are covered, and indexes the indeterminates by an arbitrary type, which may be infinite. A polynomial is literally a finitely supported function from exponent vectors to coefficients, and exponent vectors are themselves finitely supported functions from the index type to the natural numbers; multiplication is the convolution of the monoid algebra of the exponent vectors. Polynomials in one indeterminate form a separate type, related to the several-indeterminate version with a one-element index type by an isomorphism of algebras. The total degree is a natural number, and the zero polynomial is given total degree \(0\), so the additivity of total degree under multiplication requires both factors to be nonzero. The integral domain property holds over any semiring that is a domain and has cancellative addition, which for a ring is automatic.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMvPolynomial
Uses 2 · Used by 12
Statement usesRing · Finitely supported function
Used byExistence of algebraic closure of a field · Chevalley-Warning theorem (Number theory) · Matiyasevič's theorem · Ring of Witt vectors · \(A[{X_i}]\) is a UFD when \(A\) is a UFD · Nullstellensatz · Chevalley–Warning theorem (1000+ theorems) · Schwartz–Zippel theorem · Ax–Grothendieck theorem · Decomposition into sums of homogeneous polynomials · Newton's identities · Symmetric polynomials

AbbreviationPower series#

A formal power series in one indeterminate \(X\) over a ring \(R\) is an expression \(\sum_{n \ge 0} a_n X^n\) with coefficients \(a_n\) in \(R\), added and multiplied as if it were a polynomial that never ends. Nothing is evaluated and no question of convergence arises: a power series is just its sequence of coefficients, and the set \(R[[X]]\) of all such series is made into a ring by a multiplication that extends that of polynomials. Formal power series extend polynomials, serve as generating functions in combinatorics, and supply the basic examples of complete local rings in commutative algebra.

Definition

Let \(R\) be a ring. A formal power series over \(R\) is a sequence \((a_0, a_1, a_2, \dots)\) of elements of \(R\), written \(f = \sum_{n \ge 0} a_n X^n\). The element \(a_n\) is the \(n\)th coefficient of \(f\), and \(a_0\) is its constant coefficient. Two power series with the same coefficients are equal. Addition is coefficientwise, and multiplication is the Cauchy product

\[\Big(\sum_{n \ge 0} a_n X^n\Big)\Big(\sum_{n \ge 0} b_n X^n\Big) = \sum_{n \ge 0} c_n X^n, \qquad c_n = \sum_{i + j = n} a_i b_j .\]

That is, the \(n\)th coefficient of a product is \(\sum_{i+j=n} a_i b_j\), a finite sum, so the product is defined without any limit. With these operations the formal power series over \(R\) form a ring \(R[[X]]\), commutative when \(R\) is. The polynomial ring \(R[X]\) sits inside it: sending a polynomial to the power series with the same coefficients is injective and respects multiplication.

Examples
  • Geometric series. Over a commutative ring, \((1 + X + X^2 + \cdots)(1 - X) = 1\). So \(1 - X\) is a unit in \(R[[X]]\), although for \(R \neq 0\) it is not a unit in \(R[X]\).
  • Exponential series. Over a ring containing the rational numbers, the series \(e^X = \sum_{n \ge 0} X^n / n!\) makes sense. When the ring is commutative, its formal derivative (the series \(\sum_{n \ge 0} (n+1) a_{n+1} X^n\) for \(f = \sum a_n X^n\)) is \(e^X\) itself, and for elements \(a\) and \(b\) of the ring, \(e^{aX} e^{bX} = e^{(a+b)X}\), where \(e^{aX}\) is the series with \(n\)th coefficient \(a^n / n!\).
  • Generating functions. The series \(C(X) = \sum_{n \ge 0} C_n X^n\) whose coefficients are the Catalan numbers satisfies \(C(X) = 1 + X\,C(X)^2\), the identity that encodes their recursion. Euler's pentagonal number theorem is likewise an identity between an infinite product and an infinite sum of power series.
Properties
  • Units. A series is a unit if and only if its constant coefficient is a unit of \(R\). If \(a_0\) is invertible, the coefficients of the inverse \(\sum b_n X^n\) are found one at a time from \(a_0 b_0 = 1\) and \(a_0 b_n + a_1 b_{n-1} + \cdots + a_n b_0 = 0\) for \(n \ge 1\).
  • Divisibility by \(X\). The series \(f\) is divisible by \(X\) exactly when its constant coefficient is \(0\), and more generally \(X^n\) divides \(f\) exactly when \(a_0, \dots, a_{n-1}\) all vanish.
  • Order. The order of a nonzero series is the least \(n\) with \(a_n \neq 0\); the zero series has order \(\infty\). If \(R\) has no zero divisors, then the order of a product is the sum of the orders, so a product of nonzero series is nonzero. Hence \(R[[X]]\) is an integral domain whenever \(R\) is, and for a commutative integral domain \(R\) the element \(X\) is prime.
  • Power series over a field. If \(k\) is a field, every nonzero series is \(X^n u\) with \(n\) its order and \(u\) a unit, so \(k[[X]]\) is a discrete valuation ring, that is, a local principal ideal domain that is not a field. Its maximal ideal is generated by \(X\), and its nonzero ideals are the ideals generated by the powers of \(X\).
  • Noetherian property. Over a commutative Noetherian ring, power series in finitely many indeterminates again form a Noetherian ring; for one indeterminate this is the power series analogue of the Hilbert basis theorem.
  • Truncations. If \(R\) is a topological space, give \(R[[X]]\) the coefficientwise (product) topology, in which a sequence of series converges exactly when, for each \(n\), the sequence of \(n\)th coefficients converges in \(R\). For \(R\) commutative, the polynomials obtained by cutting \(f\) off after more and more terms converge to \(f\). When \(R\) carries the discrete topology this is the \(X\)-adic topology, in which \(R[[X]]\) is the completion of \(R[X]\): the polynomials are dense in it, and every Cauchy sequence in it converges.

Power series in several indeterminates are defined the same way, with coefficients indexed by monomials. The formal derivative of a power series extends the polynomial derivative. The Weierstrass preparation theorem factors a power series over a complete local ring, provided its reduction modulo the maximal ideal is nonzero, as a polynomial of a special (distinguished) form times a unit. Convergent power series in analysis, which define functions on a disc and have a radius of convergence, are a separate notion; a formal power series is the purely algebraic object that remains when convergence is ignored.

In Mathlib

Mathlib defines power series in one indeterminate as the special case of power series in several indeterminates whose set of indeterminates has a single element. A series is then a function from exponents to coefficients, and a layer of basic lemmas lets one index coefficients by natural numbers as usual. The definition accepts any coefficient type; the ring structure requires \(R\) to be a semiring, so series with natural-number coefficients, such as the Catalan series, are covered directly. No topology is attached by default: the coefficientwise topology is available only when explicitly switched on. The order of a series takes values in the natural numbers extended by \(\infty\). Over a field the inverse is defined for every series, and the inverse is \(0\) exactly when the constant coefficient is \(0\), so it agrees with the true inverse precisely on the units. Convergent power series of analysis are formalized separately, as formal multilinear series.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPowerSeries
Uses 2 · Used by 4
Statement usesRing · Polynomial in one indeterminate
Used byBernoulli numbers · Weierstrass preparation theorem · Glaisher's theorem · Pentagonal number theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.